On an unsatisfiability-satisfiability prover

DOI10.2977/PRIMS/1195173764MaRDI QIDQ1264000zbMATH OpenOpenAlexFDO

Authors Chiharu Hosono

Publication date 1989

Published in Publications of the Research Institute for Mathematical Sciences, Kyoto University (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2977/prims/1195173764

zbMATH Keywords

automated theorem provingfinite domainHerbrand universe

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

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.

Recommendations

• scientific article; zbMATH DE number 4088977
• scientific article; zbMATH DE number 956865
• scientific article; zbMATH DE number 1614715
• Solving the incremental satisfiability problem
• Beyond satisfiability: extensions and applications

Cites work

• A superposition oriented theorem prover
• scientific article; zbMATH DE number 4108722 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Theorem Proving via General Matings
• Theorem proving with abstraction
• Theorem proving with variable-constrained resolution

Cited in

(6)

• scientific article; zbMATH DE number 4088977 (Why is no real title available?)
• Towards a Semantics of Unsatisfiability Proofs with Inprocessing
• scientific article; zbMATH DE number 2159161 (Why is no real title available?)
• A threshold for unsatisfiability
• Computer Science Logic
• scientific article; zbMATH DE number 2236687 (Why is no real title available?)

This page was built for publication: On an unsatisfiability-satisfiability prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1264000)