Semantically-guided goal-sensitive reasoning: model representation
From MaRDI portal
Publication:287333
DOI10.1007/s10817-015-9334-4zbMath1356.68180OpenAlexW763811073MaRDI QIDQ287333
Maria Paola Bonacina, David Alan Plaisted
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-015-9334-4
Related Items
Semantically-guided goal-sensitive reasoning: model representation, On First-Order Model-Based Reasoning, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Semantically-guided goal-sensitive reasoning: inference system and completeness, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, SCL clause learning from simple models, SGGS decision procedures, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective
Uses Software
Cites Work
- Semantically-guided goal-sensitive reasoning: model representation
- Model evolution with equality -- revised and implemented
- On deciding satisfiability by theorem proving with speculative inferences
- Deciding floating-point logic with abstract conflict driven clause learning
- Eliminating dublication with the hyper-linking strategy
- Comparing instance generation methods for automated reasoning
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Consolution as a framework for comparing calculi
- Ordered semantic hyper-linking
- Automated deduction by theory resolution
- Implementing the Davis-Putnam method
- Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
- The model evolution calculus as a first-order DPLL method
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Automated model building
- System Description: E 1.8
- EPR-Based Bounded Model Checking at Word Level
- Solving Non-linear Arithmetic
- A Model-Constructing Satisfiability Calculus
- Proof and Model Generation with Disconnection Tableaux
- Conflict Resolution
- Solving SAT and SAT Modulo Theories
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Proof Systems for Effectively Propositional Logic
- Labelled Splitting
- Engineering DPLL(T) + Saturation
- Simplify: a theorem prover for program checking
- Natural Domain SMT: A Preliminary Assessment
- Generalizing DPLL to Richer Logics
- A Unification Algorithm for Associative-Commutative Functions
- Complete Sets of Reductions for Some Equational Theories
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- 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
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- Cutting to the Chase Solving Linear Integer Arithmetic
- Theory and Applications of Satisfiability Testing
- 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 Simplified Format for the Model Elimination Theorem-Proving Procedure
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
