On First-Order Model-Based Reasoning
From MaRDI portal
Publication:2945706
DOI10.1007/978-3-319-23165-5_8zbMATH Open1322.03013arXiv1502.02535OpenAlexW3100230358MaRDI QIDQ2945706FDOQ2945706
Authors: Maria Paola Bonacina, Viorica Sofronie-Stokkermans, Ulrich Furbach 
Publication date: 14 September 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Abstract: Reasoning semantically in first-order logic is notoriously a challenge. This paper surveys a selection of semantically-guided or model-based methods that aim at meeting aspects of this challenge. For first-order logic we touch upon resolution-based methods, tableaux-based methods, DPLL-inspired methods, and we give a preview of a new method called SGGS, for Semantically-Guided Goal-Sensitive reasoning. For first-order theories we highlight hierarchical and locality-based methods, concluding with the recent Model-Constructing satisfiability calculus.
Full work available at URL: https://arxiv.org/abs/1502.02535
Recommendations
- An Ontology-Based First-Order Modal Logic
- scientific article; zbMATH DE number 1301853
- First-order logic theorem proving and model building via approximation and instantiation
- Automatic models of first order theories
- scientific article; zbMATH DE number 4058914
- scientific article; zbMATH DE number 67794
- scientific article; zbMATH DE number 2219519
- First-order resolution methods for modal logics
- Modelling Puzzles in First Order Logic
- First-order abduction as enumeration of stable models
Cites Work
- Model evolution with equality -- revised and implemented
- System description: E-KRhyper 1.4. Extensions for unique names and description logic
- Simplification by Cooperating Decision Procedures
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Handbook of knowledge representation.
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Ordered semantic hyper-linking
- 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
- Interpolation systems for ground proofs in automated deduction: a survey
- Semantically-guided goal-sensitive reasoning: model representation
- A model-constructing satisfiability calculus
- Title not available (Why is that?)
- Interpolation in local theory extensions
- Title not available (Why is that?)
- Complete Sets of Reductions for Some Equational Theories
- Title not available (Why is that?)
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Title not available (Why is that?)
- On deciding satisfiability by theorem proving with speculative inferences
- Title not available (Why is that?)
- Title not available (Why is that?)
- Superposition and Model Evolution Combined
- Lemma Learning in the Model Evolution Calculus
- On Local Reasoning in Verification
- 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?)
- Eliminating dublication with the hyper-linking strategy
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theorem proving in cancellative abelian monoids (extended abstract)
- Superposition modulo linear arithmetic SUP(LA)
- Ordered chaining calculi for first-order theories of transitive relations
- Handbook of automated reasoning. In 2 vols
- Refutational theorem proving for hierarchic first-order theories
- Sufficient-completeness, ground-reducibility and their complexity
- Term Rewriting and Applications
- Theory decision by decomposition
- Automated Deduction – CADE-20
- Title not available (Why is that?)
- Towards a foundation of completion procedures as semidecision procedures
- Theorem-proving with resolution and superposition
- Variant narrowing and equational unification
- Completion of a Set of Rules Modulo a Set of Equations
- Superposition theorem proving for abelian groups represented as integer modules
- Order-sorted equational unification revisited
- Title not available (Why is that?)
- Order-sorted unification
- Title not available (Why is that?)
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Hierarchic superposition with weak abstraction
- Hyper tableaux
- On Hierarchical Reasoning in Combinations of Theories
- Permutative rewriting and unification
- Automated deduction. A basis for applications. Vol. III: Applications
- Theorem proving techniques for view deletion in databases
- Gibbard's collapse theorem for the indicative conditional: an axiomatic approach
- The hyper tableaux calculus with equality and an application to finite model computation
- Tableaux for diagnosis applications
- MACE4 and SEM: a comparison of finite model generators
- Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
- Semantically guided evolution of \(\mathcal{SHI}\) ABoxes
- (Dual) hoops have unique halving
Cited In (16)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- SCL(EQ): SCL for first-order logic with equality
- SCL(EQ): SCL for first-order logic with equality
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Semantically-guided goal-sensitive reasoning: model representation
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Title not available (Why is that?)
- A practical integration of first-order reasoning and decision procedures
- First-order abduction as enumeration of stable models
- The model evolution calculus as a first-order DPLL method
- History and prospects for first-order automated deduction
- Title not available (Why is that?)
- First order theories for partial models
- Automatic models of first order theories
Uses Software
This page was built for publication: On First-Order Model-Based Reasoning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945706)
