Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover

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

zbMATH Keywords

first-order logicrewritingtermination toolshyperresolutionordered resolutiondecidable fragmentsSGGS

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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