reasoning.java

一个简单的推理系统,可以对简单表达式进行规约判断

            .add(layout.createSequentialGroup()
                .add(jPanel1, org.jdesktop.layout.GroupLayout.PREFERRED_SIZE, org.jdesktop.layout.GroupLayout.DEFAULT_SIZE, org.jdesktop.layout.GroupLayout.PREFERRED_SIZE)
                .addPreferredGap(org.jdesktop.layout.LayoutStyle.RELATED)
                .add(jPanel2, org.jdesktop.layout.GroupLayout.DEFAULT_SIZE, org.jdesktop.layout.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
            .add(jToolBar1, org.jdesktop.layout.GroupLayout.DEFAULT_SIZE, 567, Short.MAX_VALUE)
        );
        layout.setVerticalGroup(
            layout.createParallelGroup(org.jdesktop.layout.GroupLayout.LEADING)
            .add(layout.createSequentialGroup()
                .add(jToolBar1, org.jdesktop.layout.GroupLayout.PREFERRED_SIZE, 40, org.jdesktop.layout.GroupLayout.PREFERRED_SIZE)
                .addPreferredGap(org.jdesktop.layout.LayoutStyle.RELATED)
                .add(layout.createParallelGroup(org.jdesktop.layout.GroupLayout.LEADING)
                    .add(jPanel2, org.jdesktop.layout.GroupLayout.DEFAULT_SIZE, org.jdesktop.layout.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                    .add(jPanel1, org.jdesktop.layout.GroupLayout.DEFAULT_SIZE, org.jdesktop.layout.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)))
        );
        pack();
    }// </editor-fold>//GEN-END:initComponents

    private void jTextArea1MouseClicked(java.awt.event.MouseEvent evt) {//GEN-FIRST:event_jTextArea1MouseClicked
// TODO add your handling code here:
        jButton3.setEnabled(true);
        jButton4.setEnabled(true);
        jButton5.setEnabled(true);
        jButton6.setEnabled(true);
    }//GEN-LAST:event_jTextArea1MouseClicked

    private void jTextField1MouseClicked(java.awt.event.MouseEvent evt) {//GEN-FIRST:event_jTextField1MouseClicked
// TODO add your handling code here:
        jButton3.setEnabled(false);
        jButton4.setEnabled(false);
        jButton5.setEnabled(false);
        jButton6.setEnabled(false);
    }//GEN-LAST:event_jTextField1MouseClicked

    private void jComboBox1ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jComboBox1ActionPerformed
// TODO add your handling code here:
        jTextArea1.setText(jComboBox1.getSelectedItem().toString().trim());
        jTextField1.setText(jComboBox2.getSelectedItem().toString().trim());
    }//GEN-LAST:event_jComboBox1ActionPerformed

    private void jComboBox2ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jComboBox2ActionPerformed
// TODO add your handling code here:
        jTextArea1.setText(jComboBox1.getSelectedItem().toString().trim());
        jTextField1.setText(jComboBox2.getSelectedItem().toString().trim());
    }//GEN-LAST:event_jComboBox2ActionPerformed

    private void jComboBox1MouseClicked(java.awt.event.MouseEvent evt) {//GEN-FIRST:event_jComboBox1MouseClicked
// TODO add your handling code here:
        jTextArea1.setText(jComboBox1.getSelectedItem().toString().trim());
        jTextField1.setText(jComboBox2.getSelectedItem().toString().trim());
    }//GEN-LAST:event_jComboBox1MouseClicked
    
    private void jButton2ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jButton2ActionPerformed
// TODO add your handling code here:
        System.exit(0);
    }//GEN-LAST:event_jButton2ActionPerformed
    
    private void jButton6ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jButton6ActionPerformed
// TODO add your handling code here:
        jTextArea1.append("!");
        jTextArea1.requestFocus();
    }//GEN-LAST:event_jButton6ActionPerformed
    
    private void jButton5ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jButton5ActionPerformed
// TODO add your handling code here:
        jTextArea1.append("∧");
        jTextArea1.requestFocus();
    }//GEN-LAST:event_jButton5ActionPerformed
    
    private void jButton4ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jButton4ActionPerformed
// TODO add your handling code here:
        jTextArea1.append("∨");
        jTextArea1.requestFocus();
    }//GEN-LAST:event_jButton4ActionPerformed
    
    private void jButton3ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jButton3ActionPerformed
// TODO add your handling code here:
        jTextArea1.append("→");
        jTextArea1.requestFocus();
    }//GEN-LAST:event_jButton3ActionPerformed
    
    private void jButton1ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jButton1ActionPerformed
// TODO add your handling code here:
		jTextArea2.setText("");
        String s=jTextArea1.getText().trim();
        s=s.toLowerCase();
        String s1[]=s.split(",");
        for(int i=0;i<s1.length;i++) {
            if(s1[i].contains("→")||s1[i].contains("∧")) {
                String s12[]=dealChar(s1[i].toCharArray()).split(",");
                for(int j=0;j<s12.length;j++)
                    jTextArea2.append("T"+(i+1)+j+":"+s12[j]+"\n");
            } else
                jTextArea2.append("T"+(i+1)+":"+s1[i]+"\n");
        }
        String d=jTextField1.getText().trim();
        d=dealChar(d.toCharArray());
        //       String dis[]=d.split("∧");
        jTextArea2.append("目标:"+d+"\n");
        String kk[]=jTextArea2.getText().split("\n");
        for(int i=0;i<kk.length;i++) {
            kk[i]=kk[i].substring(kk[i].indexOf(":")+1);
            kk[i]=justify(kk[i].toCharArray());
         //   jTextArea2.append(kk[i]+"\n");
        }
		jTextArea2.append("以下以大写字母表示相应小写字母的非命题");
        int k=0;
        int mk[]=new int[2];
        mk[0]=0;
        mk[1]=0;
        String pre[]={null,null,null};
        boolean flag=false;
        String temp=kk[kk.length-1];
        int flag2=kk.length-1;
        int jm[]=new int[kk.length];
        for(int i=0;i<kk.length;i++)
            jm[i]=0;
        ALL:while(k>=0) {
			while(jm[k]<kk.length-1){                        
                BLL:for(int i=jm[k];i<kk.length-1;i++) {//在k层查找
                    jm[k]=jm[k]+1;
                    if(kk[i].contains(temp)) {
                        mk[0]=i;
                        mk[1]=flag2;
                        pre[0]=kk[i];
                        pre[1]=kk[flag2];
                        pre[2]=temp;
                        jTextArea2.append("\n"+kk[i]);
                        jTextArea2.append("  "+kk[flag2]);//将当前用于合并的两个子句显示在文本域中
                        String mm[]=kk[i].split("∨");
                        kk[i]="";
                        String temp1="!";
                        int count=0;
                        for(int j=0;j<mm.length;j++){//重新确定kk[i],kk[flag2],flag2的值
                            if(!mm[j].equals(temp)) {
                                if(count==0) {
                                    temp1+=mm[j];
                                    temp1=justify(temp1.toCharArray());
                                    flag2=i;
                                }
                                kk[i]+=mm[j];
                                count++;
                                if(count<mm.length-1)
                                    kk[i]+="∨";
                            }
                           // if(kk[mk[1]].length()>2)
                            //    kk[i]+=kk[mk[1]].substring(1);
                        }
                        if(temp1.equals("!")) {
                            if(kk[flag2].length()>2) {
                                kk[flag2]=kk[flag2].substring(2);
                                String m[]=kk[flag2].split("∨");
                                if(m.length!=0) {
                                    temp1+=m[0];
                                    temp1=justify(temp1.toCharArray());
                                    if(kk[flag2].length()>2)
                                        kk[flag2]=kk[flag2].substring(2);
                                }
                            }
                        }
                        temp=temp1;
						//jTextArea2.append(temp+"\n");
                        if(temp1.equals("!"))//两个子句都为空,归结成功,退出
                        {
                            flag=true;
                            break ALL;
                        } else {
                            k++;
                            break BLL;//跳出for循环，进行下一层的演算
                        }
                    }
                }
			}
                        if(k!=jm[k])
	    jTextArea2.append("\n上一步归结行不通！");
            jm[k]=0;
            k=k-1;
            kk[mk[0]]=pre[0];
            kk[mk[1]]=pre[1];
			temp=pre[2];
            flag2=mk[1];            
        }
        if(flag) {
            jTextArea2.append("\nnull");
            jLabel5.setText("归结成功");
        } else
            jLabel5.setText("归结失败");
    }//GEN-LAST:event_jButton1ActionPerformed
    private String dealChar(char a[]){
        String s="";
        int i;
        Stack st=new Stack();
        boolean flag=false;
        //      try{
        for(i=a.length-1;i>=0;i--) {
            if(a[i]=='→') {
                if(!st.empty())
                    st.push('∨');
                flag=true;
            } else {
                if(a[i]=='∧') {
                    if(flag)
                        st.push('∨');
                    else
                        st.push(',');
                } else{
                    if(flag) {
                        if(a[i]=='∨') {
                            String xy="";
                            while((!st.empty())) {
                                xy+=st.pop();
                            }
                            char kj[]=xy.toCharArray();
                            for(int k=kj.length-1;k>=0;k--)
                                st.push(kj[k]);
                            st.push(',');
                            int j=0;
                            while(kj[j]=='!')
                                j++;
                            for(int k=kj.length-1;k>j;k--)
                                st.push(kj[k]);
                        } else{
                            st.push(a[i]);
                            st.push('!');
                        }
                    } else{
                        st.push(a[i]);
                    }
                }
            }
        }
        while(!st.empty()) {
            s=s+st.pop();
        }
        s=change(s);
        //  }catch(Exception e){JOptionPane.showMessageDialog(this,"请确认输入是否正确!","warring",JOptionPane.WARNING_MESSAGE);}
        return s;
    }
    private String change(String k) {
        String s[]=k.split("∨");
        k="";
        for(int i=0;i<s.length;i++) {
            if(s[i].contains("!!!"))
                s[i]=s[i].substring(3);
            if(s[i].contains("!!"))
                s[i]=s[i].substring(2);
            k+=s[i];
            if(i!=s.length-1)
                k+="∨";
        }
        return k;
    }
    private String justify(char a[]) {
        String s="";
        for(int i=0;i<a.length;i++) {
            if(a[i]=='!') {
                i++;
                if(Character.isLowerCase(a[i]))
                    a[i]=Character.toUpperCase(a[i]);
                else
                    a[i]=Character.toLowerCase(a[i]);
            }
            s+=a[i];
        }
        return s;
    }    
    /**
     * @param args the command line arguments
     */
    public static void main(String args[]) {
        java.awt.EventQueue.invokeLater(new Runnable() {
            public void run() {
                new reasoning().setVisible(true);
            }
        });
    }
    
    // Variables declaration - do not modify//GEN-BEGIN:variables
    private javax.swing.JButton jButton1;
    private javax.swing.JButton jButton2;
    private javax.swing.JButton jButton3;
    private javax.swing.JButton jButton4;
    private javax.swing.JButton jButton5;
    private javax.swing.JButton jButton6;
    private javax.swing.JComboBox jComboBox1;
    private javax.swing.JComboBox jComboBox2;
    private javax.swing.JDialog jDialog1;
    private javax.swing.JFileChooser jFileChooser1;
    private javax.swing.JLabel jLabel1;
    private javax.swing.JLabel jLabel10;
    private javax.swing.JLabel jLabel2;
    private javax.swing.JLabel jLabel3;
    private javax.swing.JLabel jLabel4;
    private javax.swing.JLabel jLabel5;
    private javax.swing.JLabel jLabel6;
    private javax.swing.JLabel jLabel7;
    private javax.swing.JLabel jLabel8;
    private javax.swing.JLabel jLabel9;
    private javax.swing.JPanel jPanel1;
    private javax.swing.JPanel jPanel2;
    private javax.swing.JScrollPane jScrollPane1;
    private javax.swing.JScrollPane jScrollPane2;
    private javax.swing.JTextArea jTextArea1;
    private javax.swing.JTextArea jTextArea2;
    private javax.swing.JTextField jTextField1;
    private javax.swing.JToolBar jToolBar1;
    // End of variables declaration//GEN-END:variables
    
}