scholarly journals DLS-Forgetter: An Implementation of the DLS Forgetting Calculus for First-Order Logic

10.29007/hvz6 ◽  
2019 ◽  
Author(s):  
Ruba Alassaf ◽  
Renate A. Schmidt
Keyword(s):  
Modal Logic ◽  
Information Hiding ◽  
Empirical Evaluation ◽  
Research Community ◽  
Order Logic ◽  
First Order Logic ◽  
Inference System ◽  
First Order ◽  
Experimental Tool ◽  
Logic Inference

DLS-Forgetter is a reasoning tool that aims to compute restricted views of a knowledge base of first-order logic formulae via semantic forgetting. Semantic forgetting achieves this by eliminating predicate symbols in an equivalence preserving way up to the remain- ing symbols. Forgetting has many applications such as information hiding, explanation generation and computing logical difference. DLS-Forgetter combines ideas from two Ackermann-based approaches: the DLS algorithm and a modal logic inference system inspired by the algorithm. The tool enhances the DLS algorithm by incorporating an ordering over the symbols in the forgetting signature. This allows more control over the forgetting process and the application of the elimination rules. The theory behind the tool is provided by a first-order Ackermann calculus, a first-order generalisation of the rules outlined by the modal logic inference system. The purpose of the tool is to provide the research community with an experimental tool to allow further research to be conducted in the area. This paper describes the DLS-Forgetter tool along with its underlying calculus, it outlines the forgetting process used in the implementation, and presents results of an empirical evaluation.

scholarly journals Formula size games for modal logic and μ-calculus

2019 ◽  
Vol 29 (8) ◽  
pp. 1311-1344 ◽  
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 $.

Logical Tools

2021 ◽  
pp. 14-52
Author(s):  
Cian Dorr ◽  
John Hawthorne ◽  
Juhani Yli-Vakkuri
Keyword(s):  
Modal Logic ◽  
Possible Worlds ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
System P

This chapter presents the system of classical higher-order modal logic which will be employed throughout this book. Nothing more than a passing familiarity with classical first-order logic and standard systems of modal logic is presupposed. We offer some general remarks about the kind of commitment involved in endorsing this logic, and motivate some of its more non-standard features. We also discuss how talk about possible worlds can be represented within the system.

Lifting propositional proof compression algorithms to first-order logic

2020 ◽  
Author(s):  
Jan Gorzny ◽  
Ezequiel Postan ◽  
Bruno Woltzenlogel Paleo
Keyword(s):  
Propositional Logic ◽  
Empirical Evaluation ◽  
Order Logic ◽  
Automated Deduction ◽  
First Order Logic ◽  
Compression Algorithms ◽  
International Conference ◽  
First Order ◽  
Theorem Provers ◽  
Resolution Proofs

Abstract Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. The first approach lifted from propositional logic delays resolution with unit clauses, which are clauses that have a single literal. The second approach is partial regularization, which removes an inference $\eta $ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from $\eta $ to the root of the proof. This paper describes the generalization of the algorithms LowerUnits and RecyclePivotsWithIntersection (Fontaine et al.. Compression of propositional resolution proofs via partial regularization. In Automated Deduction—CADE-23—23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31–August 5, 2011, p. 237--251. Springer, 2011) from propositional logic to first-order logic. The generalized algorithms compresses resolution proofs containing resolution and factoring inferences with unification. An empirical evaluation of these approaches is included.

scholarly journals Tableau-based translation from first-order logic to modal logic

2021 ◽  
Vol 56 ◽  
pp. 57-74
Author(s):  
Tin Perkov ◽  
Luka Mikec
Keyword(s):  
Modal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Modal Formula ◽  
First Order ◽  
Starting Point ◽  
Invariance Test

We define a procedure for translating a given first-order formula to an equivalent modal formula, if one exists, by using tableau-based bisimulation invariance test. A previously developed tableau procedure tests bisimulation invariance of a given first-order formula, and therefore tests whether that formula is equivalent to the standard translation of some modal formula. Using a closed tableau as the starting point, we show how an equivalent modal formula can be effectively obtained.

scholarly journals A Quantified Coalgebraic van Benthem Theorem

2021 ◽  
pp. 551-571
Author(s):  
Paul Wild ◽  
Lutz Schröder
Keyword(s):  
Modal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Transition Systems ◽  
First Order ◽  
Wide Range ◽  
Symmetry Assumption ◽  
Invariant Properties ◽  
Bounded Rank

AbstractThe classical van Benthem theorem characterizes modal logic as the bisimulation-invariant fragment of first-order logic; put differently, modal logic is as expressive as full first-order logic on bisimulation-invariant properties. This result has recently been extended to two flavours of quantitative modal logic, viz. fuzzy modal logic and probabilistic modal logic. In both cases, the quantitative van Benthem theorem states that every formula in the respective quantitative variant of first-order logic that is bisimulation-invariant, in the sense of being nonexpansive w.r.t. behavioural distance, can be approximated by quantitative modal formulae of bounded rank. In the present paper, we unify and generalize these results in three directions: We lift them to full coalgebraic generality, thus covering a wide range of system types including, besides fuzzy and probabilistic transition systems as in the existing examples, e.g. also metric transition systems; and we generalize from real-valued to quantale-valued behavioural distances, e.g. nondeterministic behavioural distances on metric transition systems; and we remove the symmetry assumption on behavioural distances, thus covering also quantitative notions of simulation.

scholarly journals Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

10.29007/cpbz ◽  
2018 ◽  
Author(s):  
Damien Doligez ◽  
Jael Kriener ◽  
Leslie Lamport ◽  
Tomer Libal ◽  
Stephan Merz
Keyword(s):  
Modal Logic ◽  
Modal Logics ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Propositional Modal Logic ◽  
Theorem Provers ◽  
Syntactic Abstraction

We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic.

scholarly journals SOME MODEL THEORY OF GUARDED NEGATION

2018 ◽  
Vol 83 (04) ◽  
pp. 1307-1344
Author(s):  
VINCE BÁRÁNY ◽  
MICHAEL BENEDIKT ◽  
BALDER TEN CATE
Keyword(s):  
Modal Logic ◽  
Model Theory ◽  
Description Logics ◽  
Expressive Power ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Beth Definability ◽  
Order Translations ◽  
Certain Answers

AbstractThe Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this article we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics.

scholarly journals Modal Homotopy Type Theory

2020 ◽  
Author(s):  
David Corfield
Keyword(s):  
Modal Logic ◽  
Homotopy Type ◽  
Type Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Bertrand Russell ◽  
First Order ◽  
Homotopy Type Theory ◽  
General Variation

In[KF1] 1914, in an essay entitled ‘Logic as the Essence of Philosophy’, Bertrand Russell promised to revolutionize philosophy by introducing there the ‘new logic’ of Frege and Peano: “The old logic put thought in fetters, while the new logic gives it wings.” A century later, this book proposes a comparable revolution with a newly emerging logic, modal homotopy type theory. Russell’s prediction turned out to be accurate. Frege’s first-order logic, along with its extension to modal logic, is to be found throughout anglophone analytic philosophy. This book provides a considerable array of evidence for the claim that philosophers working in metaphysics, as well as those treating language, logic or mathematics, would be much better served with the new ‘new logic’. It offers an introduction to this new logic, thoroughly motivated by intuitive explanations of the need for all of its component parts—the discipline of a type theory, the flexibility of type dependency, the more refined homotopic notion of identity and a powerful range of modalities. Innovative applications of the calculus are given, including analysis of the distinction between objects and events, an intrinsic treatment of structure and a conception of modality both as a form of general variation and as allowing constructions in modern geometry. In this way, we see how varied are the applications of this powerful new language—modal homotopy type theory.

scholarly journals Partial Regularization of First-Order Resolution Proofs

10.29007/3r41 ◽  
2020 ◽  
Author(s):  
Jan Gorzny ◽  
Ezequiel Postan ◽  
Bruno Woltzenlogel Paleo
Keyword(s):  
Propositional Logic ◽  
Empirical Evaluation ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Theorem Provers ◽  
Resolution Proofs

Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs, but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. An empirical evaluation of the approach is included.

Sign in / Sign up

Export Citation Format

Share Document