On an unsatisfiability-satisfiability prover (Q1264000): Difference between revisions

Summary: We study a new unsatisfiability-satisfiability prover and its basic properties. Our main results, besides the presentation of our prover, is to show that our procedure always terminates if a given set of clauses is satisfiable in some finite domain. The unsatisfiability checking of our procedure is as strong as the existing complete proof procedures, so we examine the strength of the satisfiability checking part of our procedure. We give an unsatisfiability-satisfiability prover, and show its soundness that is for any unsatisfiable set of clauses the procedure says that it is unsatisfiable, and if the procedure says that the set of clauses is satisfiable, then it is in fact satisfiable. We show that for a given set of clauses assumed to be satisfiable in a simple theory of Herbrand universe, the procedure terminates saying it is satisfiable. We show that for a given set of clauses assumed to be satisfiable in some finite domain, the procedure terminates saying it is satisfiable.