Research On Some Automated Reasoning Methods For Logic

Automated theorem proving or mechanical theorem proving is concerned with the building of computing systems that automate the process of proving theorems. Since the 1950s ATP has been one of active research topics of computer science and successfully used in mathematics, hard test and verification, software generation and verification, protocol verification, and artificial intelligence.The partial instantiation method reduces satisfiability problems for first-order logic to a series of ground-level satisfiability problems. Finding out the blockages of satisfier mappings for clause set is necessary in this method. Clause searching method proposed by us not only decides the satisfiability of clause set but also presents a model then obtains a satisfier mapping. Lattice-valued logic is not completely comparable and proper to describing thinking, judging and decision-making. Lattice-valued propositional logic system LP(X) is proposed in 1993. At present automated reasoning research about LP(X) focuses on resolution method, this thesis discusses tableau method for LP(X). The usual deduction methods such as resolution method, tableau method, sequent calculus etc emphasis on decidability instead of deduction. This thesis discusses implementing probing method and natural deduction method for relevant propositional R, and generates readable deduction sequences similar to humans'. The main content is as follows:(1) Proposing clause searching method which decides satisfiability of clause setΦand presents a model for satisfied set. This method decides satisfiability by searching one clause which can not extended fromΦ. Updating clause searching method to first-order by use of partial instantiation methods. This thesis separates predicate formulae into two parts: structures and variables hence improves unification algorithm efficiency and saves storage space. We establish a mapping of one atom onto one positive integer and one negative word onto one negative integer.(2) Proposing tableau method for lattice-valued propositional system LP(X), and all formulae is bounding implications. By introducing concepts such as Bound~s(X), Bound_s(X) and maximally consistent set, we prove this method's correctness and completeness. If truth value space L of system LP(X) is the direct product of L_i, then we can prove theorems in LP(X) by means of direct decomposition.(3) Proposing backward probing method, obtaining a proof tree consisting of formulae in deduction sequences, and generating readable deduction sequences similar to humans'. We reduce formulae redundancy by transforming formulae into binary tree forms and storing them in a dynamic array, then array subscripts stand for formulae. (4) Proposing backtrace method applied to natural deduction method. Firstly constructing a proof tree from hypothesis set, then starting from tree root we obtain formulae attributes layer by layer. The thesis implements natural deduction method for relevant natural deduction system NR and generates readable deduction sequences similar to humans'.In conclusion, this thesis proposes clause searching method to check satisfiability of clause set, lifts the new method to first-order, proposes tableau method for latticed-valued logic system LP(X), proposes backward probing method and backtrace method, generates readable proof for relevant propositional logic and has a positive meaning in the theory and application.