2015/03/10 by Andreas Teucke, Teucke, Andreas, Christoph Weidenbach +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Natural Language Processing Techniques #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1503.02971
openalex publication_date 2015/03/10 · openalex created_date 2022/10/05 · openalex updated_date 2026/07/28
In this paper we consider first-order logic theorem proving and model\nbuilding via approximation and instantiation. Given a clause set we propose its\napproximation into a simplified clause set where satisfiability is decidable.\nThe approximation extends the signature and preserves unsatisfiability: if the\nsimplified clause set is satisfiable in some model, so is the original clause\nset in the same model interpreted in the original signature. A refutation\ngenerated by a decision procedure on the simplified clause set can then either\nbe lifted to a refutation in the original clause set, or it guides a refinement\nexcluding the previously found unliftable refutation. This way the approach is\nrefutationally complete. We do not step-wise lift refutations but conflicting\ncores, finite unsatisfiable clause sets representing at least one refutation.\nThe approach is dual to many existing approaches in the literature because our\napproximation preserves unsatisfiability.\n