Exploring Automated Reasoning in First-Order Logic: Tools, Techniques and Application Areas

AbstractFormal ontologies are axiomatizations in a logic-based formalism. The development of formal ontologies is generating considerable research on the use of automated reasoning techniques and tools that help in ontology engineering. One of the main aims is to refine and to improve axiomatizations for enabling automated reasoning tools to efficiently infer reliable information. Defects in the axiomatization cannot only cause wrong inferences, but can also hinder the inference of expected information, either by increasing the computational cost of or even preventing the inference. In this paper, we introduce a novel, fully automatic white-box testing framework for first-order logic (FOL) ontologies. Our methodology is based on the detection of inference-based redundancies in the given axiomatization. The application of the proposed testing method is fully automatic since (i) the automated generation of tests is guided only by the syntax of axioms and (ii) the evaluation of tests is performed by automated theorem provers (ATPs). Our proposal enables the detection of defects and serves to certify the grade of suitability—for reasoning purposes—of every axiom. We formally define the set of tests that are (automatically) generated from any axiom and prove that every test is logically related to redundancies in the axiom from which the test has been generated. We have implemented our method and used this implementation to automatically detect several non-trivial defects that were hidden in various FOL ontologies. Throughout the paper we provide illustrative examples of these defects, explain how they were found and how each proof—given by an ATP—provides useful hints on the nature of each defect. Additionally, by correcting all the detected defects, we have obtained an improved version of one of the tested ontologies: Adimen-SUMO.

Download Full-text

Logtk : A Logic ToolKit for Automated Reasoning and its Implementation

10.29007/4z1m ◽

2018 ◽

Author(s):

Simon Cruanes

Keyword(s):

Data Structures ◽

Automated Reasoning ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Design And Implementation ◽

Data Structures And Algorithms ◽

Index Terms

We describe the design and implementation of Logtk, an OCaml library for writing automated reasoning tools that deal with (possibly typed) first-order logic. The library provides data structures and algorithms to represent terms, formulas, substitutions, perform unification, index terms, parse problems, as well as a few tools to demonstrate itsuse. It is the basis of a full-fledged superposition prover.

Download Full-text

First-Order Logic Reasoning Support for the Semantic Web

Journal of Software ◽

10.3724/sp.j.1001.2008.03091 ◽

2009 ◽

Vol 19 (12) ◽

pp. 3091-3099 ◽

Cited By ~ 1

Author(s):

Gui-Hong XU ◽

Jian ZHANG

Keyword(s):

Semantic Web ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Logic Reasoning

Download Full-text

Boolean-valued structures

10.1093/oso/9780198790396.003.0013 ◽

2018 ◽

Author(s):

Tim Button ◽

Sean Walsh

Keyword(s):

Model Theory ◽

Order Logic ◽

First Order Logic ◽

Inference Rules ◽

Mathematical Concepts ◽

Semantic Framework ◽

First Order ◽

Standard Models ◽

Boolean Valued Model ◽

Semantic Values

Chapters 6-12 are driven by questions about the ability to pin down mathematical entities and to articulate mathematical concepts. This chapter is driven by similar questions about the ability to pin down the semantic frameworks of language. It transpires that there are not just non-standard models, but non-standard ways of doing model theory itself. In more detail: whilst we normally outline a two-valued semantics which makes sentences True or False in a model, the inference rules for first-order logic are compatible with a four-valued semantics; or a semantics with countably many values; or what-have-you. The appropriate level of generality here is that of a Boolean-valued model, which we introduce. And the plurality of possible semantic values gives rise to perhaps the ‘deepest’ level of indeterminacy questions: How can humans pin down the semantic framework for their languages? We consider three different ways for inferentialists to respond to this question.

Download Full-text

GAMES AND CARDINALITIES IN INQUISITIVE FIRST-ORDER LOGIC

The Review of Symbolic Logic ◽

10.1017/s1755020321000198 ◽

2021 ◽

pp. 1-28

Author(s):

IVANO CIARDELLI ◽

GIANLUCA GRILLETTI

Keyword(s):

Order Logic ◽

First Order Logic ◽

First Order

Download Full-text

Extensions in graph normal form

Logic Journal of IGPL ◽

10.1093/jigpal/jzaa054 ◽

2020 ◽

Author(s):

Michał Walicki

Keyword(s):

Normal Form ◽

Fixed Points ◽

Propositional Logic ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Special Cases

Abstract Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.

Download Full-text

Relational Chase Procedures Interpreted as Resolution with Paramodulation1

Fundamenta Informaticae ◽

10.3233/fi-1991-15203 ◽

1991 ◽

Vol 15 (2) ◽

pp. 123-138

Author(s):

Joachim Biskup ◽

Bernhard Convent

Keyword(s):

Alternative Interpretation ◽

Order Logic ◽

First Order Logic ◽

Inference Problem ◽

First Order ◽

Inference Problems ◽

The One ◽

The Relationship ◽

Theoretical Foundations ◽

Insight Into

In this paper the relationship between dependency theory and first-order logic is explored in order to show how relational chase procedures (i.e., algorithms to decide inference problems for dependencies) can be interpreted as clever implementations of well known refutation procedures of first-order logic with resolution and paramodulation. On the one hand this alternative interpretation provides a deeper insight into the theoretical foundations of chase procedures, whereas on the other hand it makes available an already well established theory with a great amount of known results and techniques to be used for further investigations of the inference problem for dependencies. Our presentation is a detailed and careful elaboration of an idea formerly outlined by Grant and Jacobs which up to now seems to be disregarded by the database community although it definitely deserves more attention.

Download Full-text

Formula size games for modal logic and μ-calculus

Journal of Logic and Computation ◽

10.1093/logcom/exz025 ◽

2019 ◽

Vol 29 (8) ◽

pp. 1311-1344 ◽

Cited By ~ 2

Author(s):

Lauri T Hella ◽

Miikka S Vilander

Keyword(s):

Modal Logic ◽

Optimal Strategy ◽

Order Logic ◽

First Order Logic ◽

Kripke Models ◽

First Order ◽

Modal Operators ◽

Crucial Difference ◽

Definition Of ◽

Person Game

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.

Download Full-text