Semantically-guided goal-sensitive reasoning: inference system and completeness
From MaRDI portal
Publication:1707598
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
theorem provingsemantic guidanceconflict-driven clause learningrefutational completenessgoal sensitivity
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
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
