On First-Order Model-Based Reasoning
From MaRDI portal
Publication:2945706
DOI10.1007/978-3-319-23165-5_8zbMath1322.03013arXiv1502.02535OpenAlexW3100230358MaRDI QIDQ2945706
Viorica Sofronie-Stokkermans, Maria Paola Bonacina, Ulrich Furbach
Publication date: 14 September 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1502.02535
Related Items (8)
History and Prospects for First-Order Automated Deduction ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ SCL(EQ): SCL for first-order logic with equality
Uses Software
Cites Work
- Interpolation systems for ground proofs in automated deduction: a survey
- Semantically-guided goal-sensitive reasoning: model representation
- Model evolution with equality -- revised and implemented
- On deciding satisfiability by theorem proving with speculative inferences
- Order-sorted unification
- Towards a foundation of completion procedures as semidecision procedures
- Eliminating dublication with the hyper-linking strategy
- Theorem-proving with resolution and superposition
- Permutative rewriting and unification
- Theory decision by decomposition
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Superposition theorem proving for abelian groups represented as integer modules
- Refutational theorem proving for hierarchic first-order theories
- Automated deduction. A basis for applications. Vol. III: Applications
- Ordered semantic hyper-linking
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- On interpolation in automated theorem proving
- The model evolution calculus as a first-order DPLL method
- Modular proof systems for partial functions with Evans equality
- Sufficient-completeness, ground-reducibility and their complexity
- Semantically Guided Evolution of $\mathcal{SHI}$ ABoxes
- A Model-Constructing Satisfiability Calculus
- Ordered chaining calculi for first-order theories of transitive relations
- The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation
- Solving SAT and SAT Modulo Theories
- Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
- Interpolation in local theory extensions
- Superposition Modulo Linear Arithmetic SUP(LA)
- Completion of a Set of Rules Modulo a Set of Equations
- Simplification by Cooperating Decision Procedures
- Complete Sets of Reductions for Some Equational Theories
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Tableaux for diagnosis applications
- Theorem proving in cancellative abelian monoids (extended abstract)
- MACE4 and SEM: A Comparison of Finite Model Generators
- (Dual) Hoops Have Unique Halving
- Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach
- Hierarchic Superposition with Weak Abstraction
- System Description: E-KRHyper 1.4
- Order-sorted Equational Unification Revisited
- Variant Narrowing and Equational Unification
- Superposition and Model Evolution Combined
- Hyper tableaux
- Lemma Learning in the Model Evolution Calculus
- Automated Deduction – CADE-20
- On Local Reasoning in Verification
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- A Machine-Oriented Logic Based on the Resolution Principle
- Automatic Theorem Proving With Renamable and Semantic Resolution
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Term Rewriting and Applications
- On Hierarchical Reasoning in Combinations of Theories
- Theorem proving techniques for view deletion in databases
- 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
This page was built for publication: On First-Order Model-Based Reasoning
