Semantically-guided goal-sensitive reasoning: inference system and completeness

DOI10.1007/s10817-016-9384-2zbMath1437.68189OpenAlexW2483513769MaRDI QIDQ1707598

Maria Paola Bonacina, David Alan Plaisted

Publication date: 3 April 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-016-9384-2

zbMATH Keywords

theorem provingsemantic guidanceconflict-driven clause learningrefutational completenessgoal sensitivity

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ On First-Order Model-Based Reasoning ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ SGGS decision procedures ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective

Uses Software

• OTTER
• VAMPIRE
• SPASS
• Darwin
• SATCHMO
• DCTP
• E-Darvin
• Chaff
• iProver-Eq
• iProver
• E Theorem Prover
• CLIN
• E-KRHyper

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Semantically-guided goal-sensitive reasoning: model representation
• Model evolution with equality -- revised and implemented
• On deciding satisfiability by theorem proving with speculative inferences
• Eliminating dublication with the hyper-linking strategy
• Comparing instance generation methods for automated reasoning
• Deciding effectively propositional logic using DPLL and substitution sets
• Theory decision by decomposition
• Equational problems and disunification
• Ordered semantic hyper-linking
• The model evolution calculus as a first-order DPLL method
• System Description: E 1.8
• On First-Order Model-Based Reasoning
• NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
• Proof and Model Generation with Disconnection Tableaux
• Playing with AVATAR
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Labelled Splitting
• Engineering DPLL(T) + Saturation
• GRASP: a search algorithm for propositional satisfiability
• The disconnection method
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• The Relative Power of Semantics and Unification
• System Description: E-KRHyper 1.4
• The 481 Ways to Split a Clause and Deal with Propositional Variables
• Superposition and Model Evolution Combined
• Theory Instantiation
• Lemma Learning in the Model Evolution Calculus
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Automatic Theorem Proving With Renamable and Semantic Resolution
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality