Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
From MaRDI portal
Publication:6156634
DOI10.1007/s10817-022-09656-wOpenAlexW4315498480MaRDI QIDQ6156634
Maria Paola Bonacina, Sarah Winkler
Publication date: 14 June 2023
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-022-09656-w
Cites Work
- Semantically-guided goal-sensitive reasoning: model representation
- On deciding satisfiability by theorem proving with speculative inferences
- Orderings for term-rewriting systems
- Eliminating dublication with the hyper-linking strategy
- On word problems in Horn theories
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Fast congruence closure and extensions
- Deciding effectively propositional logic using DPLL and substitution sets
- Decidable fragments of many-sorted logic
- Logic for improving integrity checking in relational data bases
- Modal languages and bounded fragments of predicate logic
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- A fully syntactic AC-RPO.
- Abstract congruence closure
- Ordered semantic hyper-linking
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Deciding the guarded fragments by resolution
- SGGS decision procedures
- Blocking and other enhancements for bottom-up model generation methods
- Conflict-driven satisfiability for theory combination: transition system and completeness
- SCL clause learning from simple models
- Faster, higher, stronger: E 2.3
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- The model evolution calculus as a first-order DPLL method
- Automated model building
- Solvable cases of the decision problem
- Non-cyclic Sorts for First-Order Satisfiability
- A Model-Constructing Satisfiability Calculus
- On First-Order Model-Based Reasoning
- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
- BDI: a new decidable clause class
- The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation
- Playing with AVATAR
- Solving SAT and SAT Modulo Theories
- Modal Tableau Systems with Blocking and Congruence Closure
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Proof Systems for Effectively Propositional Logic
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Fast Decision Procedures Based on Congruence Closure
- Variations on the Common Subexpression Problem
- Resolution Strategies as Decision Procedures
- Proving refutational completeness of theorem-proving strategies
- On the Decision Problem for Two-Variable First-Order Logic
- Canonical Ground Horn Theories
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
- First-Order Resolution Methods for Modal Logics
- Implementing Superposition in iProver (System Description)
- Hyper tableaux
- Splitting on Demand in SAT Modulo Theories
- Lemma Learning in the Model Evolution Calculus
- A Machine-Oriented Logic Based on the Resolution Principle
- Automatic Theorem Proving With Renamable and Semantic Resolution
- A machine program for theorem-proving
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
