Browse Theses

The first refutationally complete inference systems for first-order logic, called instance-based systems, were based on Herbrand's theorem which implies that first-order logic satisfiability can be reduced to propositional logic satisfiability (SAT). Out of this line of research came the landmark SAT solving DPLL algorithm. Soon after DPLL made its debut, Robinson introduced the simple combinatorial resolution rule which detracted interest in instance-based systems. Recently, with the increase in computational power of the personal computer, there has been renewed interest in systems for first-order logic theorem proving that utilize SAT solvers. Here, we present three novel solutions for the first-order logic validity problem that utilize SAT.

As our first solution, we reduce first-order logic validity to SAT, by encoding a proof of first-order logic unsatisfiability in propositional logic and use a SAT solver to determine if the encoding is satisfiable. Specifically we encode a closed connection tableaux proof of unsatisfiability. A satisfiable propositional encoding implies validity of the first-order problem. We provide an encoding using SAT, provide soundness and completeness proofs, and discuss our implementation, called CHEWTPTP-SAT, along with results. We also give an encoding in SMT, provide soundness and completeness proofs, discuss our implementation, CHEWTPTP-SMT, and discuss when then encoding in SMT may be better than an encoding in SAT.

The second solution is an inference system, called SIG-Res, which combines SInst-Gen (which utilizes SAT) with resolution into a single sound and refutationally complete system. We allow a set of clauses, S , to be distributed among two sets P and R in any combination so long as S = _P ý R . SInst-Gen is run on P with conclusions added to P , resolution is run on R with conclusions added to R , and resolution is run on P × R with conclusions added to P . Factoring is also used on all conclusions to resolution inferences. Since any distribution is allowed, this system permits a spectrum of choices. At the ends of the spectrum, for instance if P = S , the system is simply a SInst-Gen solver and if R = S , the solver is a resolution solver. We give the inference rules for SIG-Res, provide soundness and completeness proofs, and discuss an implementation, called Spectrum, along with experimental results. We also discuss a newer implementation, called EVC3, which combines the SMT solver named CVC3 with the equational theorem prover, E.

Our third solution establishes a framework, called ý + ý, which allows a wide range of first-order logic calculi to be combined into a single sound and refutationally complete system. This framework can be used to combine instance generation methods that use SAT with other inference systems. In order to combine two systems, ý and ý, into a single system, we require ý to be productive and require ý to have both the lifting and total-saturation properties. This framework allows a set of clauses to be distributed among two sets, P and R , like SIG-Res, so that ý can be used on P and ý can be used on R . A limited amount of information is passed between the systems to establish completeness of the combined system. We give the inference rules for ý + ý, establish soundness and completeness, and show how Inst-Gen-Eq and superposition can be combined in this framework.