Semantically-guided goal-sensitive reasoning: inference system and completeness
DOI10.1007/S10817-016-9384-2zbMATH Open1437.68189OpenAlexW2483513769MaRDI QIDQ1707598FDOQ1707598
Authors: Maria Paola Bonacina, David A. 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
Recommendations
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)
Cites Work
- Title not available (Why is that?)
- Model evolution with equality -- revised and implemented
- Title not available (Why is that?)
- System description: E 1.8
- System description: E-KRhyper 1.4. Extensions for unique names and description logic
- GRASP: a search algorithm for propositional satisfiability
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Ordered semantic hyper-linking
- The model evolution calculus as a first-order DPLL method
- Title not available (Why is that?)
- Combining superposition, sorts and splitting
- Semantically-guided goal-sensitive reasoning: model representation
- Proof and model generation with disconnection tableaux
- The universal computer. The road from Leibniz to Turing.
- Title not available (Why is that?)
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Labelled Splitting
- Engineering DPLL(T) + Saturation
- Title not available (Why is that?)
- Title not available (Why is that?)
- On deciding satisfiability by theorem proving with speculative inferences
- Title not available (Why is that?)
- The disconnection method
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- The Relative Power of Semantics and Unification
- The 481 ways to split a clause and deal with propositional variables
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- Eliminating dublication with the hyper-linking strategy
- Comparing instance generation methods for automated reasoning
- On First-Order Model-Based Reasoning
- Deciding effectively propositional logic using DPLL and substitution sets
- Theory decision by decomposition
- Equational problems and disunification
- Playing with AVATAR
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
Cited In (11)
- Blocking and other enhancements for bottom-up model generation methods
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Title not available (Why is that?)
- Semantically-guided goal-sensitive reasoning: model representation
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Contradiction separation based dynamic multi-clause synergized automated deduction
- On First-Order Model-Based Reasoning
- The problem of finding a semantic strategy for focusing inference rules
- SGGS decision procedures
Uses Software
This page was built for publication: Semantically-guided goal-sensitive reasoning: inference system and completeness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1707598)
