On First-Order Model-Based Reasoning

DOI10.1007/978-3-319-23165-5_8MaRDI QIDQ2945706zbMATH OpenOpenAlexFDO

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)

Full work available at URL https://arxiv.org/abs/1502.02535

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

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.

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

• scientific article; zbMATH DE number 4155933 (Why is no real title available?)
• scientific article; zbMATH DE number 3898849 (Why is no real title available?)
• scientific article; zbMATH DE number 8800 (Why is no real title available?)
• scientific article; zbMATH DE number 1303342 (Why is no real title available?)
• scientific article; zbMATH DE number 599028 (Why is no real title available?)
• scientific article; zbMATH DE number 1037485 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 2090309 (Why is no real title available?)
• scientific article; zbMATH DE number 1418280 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• (Dual) hoops have unique halving
• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• A machine program for theorem-proving
• A model-constructing satisfiability calculus
• Automated Deduction – CADE-20
• Automated deduction. A basis for applications. Vol. III: Applications
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Complete Sets of Reductions for Some Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Eliminating dublication with the hyper-linking strategy
• Gibbard's collapse theorem for the indicative conditional: an axiomatic approach
• Handbook of automated reasoning. In 2 vols
• Handbook of knowledge representation.
• Hierarchic superposition with weak abstraction
• Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
• Hyper tableaux
• Interpolation in local theory extensions
• Interpolation systems for ground proofs in automated deduction: a survey
• Lemma Learning in the Model Evolution Calculus
• MACE4 and SEM: a comparison of finite model generators
• Model evolution with equality -- revised and implemented
• Modular proof systems for partial functions with Evans equality
• On Hierarchical Reasoning in Combinations of Theories
• On Local Reasoning in Verification
• On deciding satisfiability by theorem proving with speculative inferences
• On interpolation in automated theorem proving
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Order-sorted equational unification revisited
• Order-sorted unification
• Ordered chaining calculi for first-order theories of transitive relations
• Ordered semantic hyper-linking
• Permutative rewriting and unification
• Proving refutational completeness of theorem-proving strategies
• Refutational theorem proving for hierarchic first-order theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Semantically guided evolution of \(\mathcal{SHI}\) ABoxes
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Semantically-guided goal-sensitive reasoning: model representation
• Simplification by Cooperating Decision Procedures
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Sufficient-completeness, ground-reducibility and their complexity
• Superposition and Model Evolution Combined
• Superposition modulo linear arithmetic SUP(LA)
• Superposition theorem proving for abelian groups represented as integer modules
• System description: E-KRhyper 1.4. Extensions for unique names and description logic
• Tableaux for diagnosis applications
• Term Rewriting and Applications
• The hyper tableaux calculus with equality and an application to finite model computation
• The model evolution calculus as a first-order DPLL method
• Theorem proving in cancellative abelian monoids (extended abstract)
• Theorem proving techniques for view deletion in databases
• Theorem-proving with resolution and superposition
• Theory decision by decomposition
• Towards a foundation of completion procedures as semidecision procedures
• Variant narrowing and equational unification

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
• scientific article; zbMATH DE number 5827849 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 1301853 (Why is no real title available?)
• First order theories for partial models
• Automatic models of first order theories

Describes a project that uses

Uses Software

• E-KRHyper
• SCC
• ITP
• Chaff
• Mace4
• E-Darvin
• SCOTT
• OTTER

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)