scholarly journals A Complete Cyclic Proof System for Inductive Entailments in First Order Logic

10.29007/xgc6 ◽  
2018 ◽  
Author(s):  
Radu Iosif ◽  
Cristina Serban
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Proof System ◽  
Inference Rules ◽  
Tree Automata ◽  
Top Down ◽  
Inductive System ◽  
First Order ◽  
Inductive Definitions ◽  
Small Set

In this paper we develop a cyclic proof system for the problem of inclusion between the least sets of models of mutually recursive predicates, when the ground constraints in the inductive definitions are quantifier-free formulae of first order logic. The proof system consists of a small set of inference rules, inspired by a top-down language inclusion algorithm for tree automata [9]. We show the proof system to be sound, in general, and complete, under certain semantic restrictions involving the set of constraints in the inductive system. Moreover, we investigate the computational complexity of checking these restrictions, when the function symbols in the logic are given the canonical Herbrand interpretation.

Boolean-valued structures

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.

μ-definable sets of integers

1993 ◽  
Vol 58 (1) ◽  
pp. 291-313 ◽  
Author(s):  
Robert S. Lubarsky
Keyword(s):  
Fixed Point ◽  
Free Variable ◽  
Order Logic ◽  
First Order Logic ◽  
Inductive Definition ◽  
Natural Class ◽  
First Order ◽  
Inductive Definitions ◽  
Definable Sets ◽  
The Universe

Inductive definability has been studied for some time already. Nonetheless, there are some simple questions that seem to have been overlooked. In particular, there is the problem of the expressibility of the μ-calculus.The μ-calculus originated with Scott and DeBakker [SD] and was developed by Hitchcock and Park [HP], Park [Pa], Kozen [K], and others. It is a language for including inductive definitions with first-order logic. One can think of a formula in first-order logic (with one free variable) as defining a subset of the universe, the set of elements that make it true. Then “and” corresponds to intersection, “or” to union, and “not” to complementation. Viewing the standard connectives as operations on sets, there is no reason not to include one more: least fixed point.There are certain features of the μ-calculus coming from its being a language that make it interesting. A natural class of inductive definitions are those that are monotone: if X ⊃ Y then Γ (X) ⊃ Γ (Y) (where Γ (X) is the result of one application of the operator Γ to the set X). When studying monotonic operations in the context of a language, one would need a syntactic guarantor of monotonicity. This is provided by the notion of positivity. An occurrence of a set variable S is positive if that occurrence is in the scopes of exactly an even number of negations (the antecedent of a conditional counting as a negation). S is positive in a formula ϕ if each occurrence of S is positive. Intuitively, the formula can ask whether x ∊ S, but not whether x ∉ S. Such a ϕ can be considered an inductive definition: Γ (X) = {x ∣ ϕ(x), where the variable S is interpreted as X}. Moreover, this induction is monotone: as X gets bigger, ϕ can become only more true, by the positivity of S in ϕ. So in the μ-calculus, a formula is well formed by definition only if all of its inductive definitions are positive, in order to guarantee that all inductive definitions are monotone.

scholarly journals VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC

2002 ◽  
Vol 13 (03) ◽  
pp. 315-340 ◽  
Author(s):  
J. I. DEN HARTOG ◽  
E. P. DE VINK
Keyword(s):  
Programming Language ◽  
Denotational Semantics ◽  
Order Logic ◽  
First Order Logic ◽  
Proof System ◽  
Probabilistic Choice ◽  
First Order ◽  
Probabilistic Programs

Probability, be it inherent or explicitly introduced, has become an important issue in the verification of programs. In this paper we study a formalism which allows reasoning about programs which can act probabilistically. To describe probabilistic programs, a basic programming language with an operator for probabilistic choice is introduced and a denotational semantics is given for this language. To specify propertics of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates is introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to be sound and complete; the properties that can be derived are exactly the valid properties. Finally some typical examples illustrate the use of the probabilistic predicates and the proof system.

scholarly journals Making Higher-Order Superposition Work

2021 ◽  
pp. 415-432
Author(s):  
Petar Vukmirović ◽  
Alexander Bentkamp ◽  
Jasmin Blanchette ◽  
Simon Cruanes ◽  
Visa Nummelin ◽  
...  
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
Inference Rules ◽  
Higher Order Logic ◽  
First Order ◽  
New Challenges

AbstractSuperposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

The Incompleteness of Peano Arithmetic with Exponentiation

1992 ◽  
Author(s):  
Raymond M. Smullyan
Keyword(s):  
Axiom System ◽  
Peano Arithmetic ◽  
Order Logic ◽  
First Order Logic ◽  
Inference Rules ◽  
First Order ◽  
Axiom Scheme

We shall now turn to a formal axiom system which we call Peano Arithmetic with Exponentiation and which we abbreviate “P.E.”. We take certain correct formulas which we call axioms and provide two inference rules that enable us to prove new correct formulas from correct formulas already proved. The axioms will be infinite in number, but each axiom will be of one of nineteen easily recognizable forms; these forms are called axiom schemes. It will be convenient to classify these nineteen axiom schemes into four groups (cf. discussion that follows the display of the schemes). The axioms of Groups I and II are the so-called logical axioms and constitute a neat formalization of first-order logic with identity due to Kalish and Montague [1965], which is based on an earlier system due to Tarski [1965]. The axioms of Groups III and IV are the so-called arithmetic axioms. In displaying these axiom schemes, F, G and H are any formulas, vi and vj are any variables, and t is any term. For example, the first scheme L1 means that for any formulas F and G, the formula (F ⊃ (G ⊃ F)) is to be taken as an axiom; axiom scheme L4 means that for any variable Vi and any formulas F and G, the formula . . . (∀vi (F ⊃ G) ⊃ (∀vi (F ⊃ ∀vi G) . . . is to be taken as an axiom.

scholarly journals Evaluating Automated Theorem Provers Using Adimen-SUMO

10.29007/hplh ◽  
2018 ◽  
Author(s):  
Javier Álvez ◽  
Paqui Lucio ◽  
German Rigau
Keyword(s):  
Order Logic ◽  
Experimental Results ◽  
First Order Logic ◽  
First Order ◽  
Theorem Provers ◽  
Small Set

We report on the results of evaluating the performance automated theorem provers using \ADIMENSUMO{}. The evaluation follows the adaptation of the methodology based on competency questions \cite{GrF95} to the framework of first-order logic, which is presented in \cite{ALR15}, and is applied to \ADIMENSUMO{} \cite{ALR12}. The set of competency questions used for this evaluation has been semi-automatically generated from a small set of semantic patterns and the mapping of \WORDNET{} to \SUMO{}, also introduced in \cite{ALR15}. Our experimental results demonstrate that improved versions of the proposed set of competency questions could be really valuable for the development of automated theorem provers.

scholarly journals Compiling Input* FO(·) inductive definitions into tabled prolog rules for IDP3

2013 ◽  
Vol 13 (4-5) ◽  
pp. 691-704 ◽  
Author(s):  
JOACHIM JANSEN ◽  
ALBERT JORISSEN ◽  
GERDA JANSSENS
Keyword(s):  
Order Logic ◽  
Experimental Results ◽  
First Order Logic ◽  
Partial Functions ◽  
First Order ◽  
Inductive Definitions ◽  
Input Structure ◽  
Model Generator ◽  
Unit Propagation

AbstractFO(·)IDP3extends first-order logic with inductive definitions, partial functions, types and aggregates. Its model generator IDP3 first grounds the theory and then uses search to find the models. The grounder uses Lifted Unit Propagation (LUP) to reduce the size of the groundings of problem specifications in IDP3. LUP is in general very effective, but performs poorly on definitions of predicates whose two-valued interpretation can be computed from data in the input structure. To solve this problem, a preprocessing step is introduced that converts such definitions to Prolog code and usesXSBProlog to compute their interpretation. The interpretation of these predicates is then added to the input structure, their definitions are removed from the theory and further processing is done by the standard IDP3 system. Experimental results show the effectiveness of our method.

scholarly journals First Order Logic with Inductive Definitions for Model-Based Problem Solving

AI Magazine ◽  
2016 ◽  
Vol 37 (3) ◽  
pp. 69-80 ◽  
Author(s):  
Maurice Bruynooghe ◽  
Marc Denecker ◽  
Miroslaw Truszczynski
Keyword(s):  
Problem Solving ◽  
Answer Set Programming ◽  
Order Logic ◽  
First Order Logic ◽  
Declarative Programming ◽  
First Order ◽  
Inductive Definitions ◽  
Trace Back ◽  
Programming Systems ◽  
Different Origins

In answer-set programming (ASP), programs can be viewed as specifications of finite Herbrand structures. Other logics can be (and, in fact, were) used towards the same end and can be taken as the basis of declarative programming systems of similar functionality as ASP. We discuss here one such logic, the logic FO(ID), and its implementation IDP3. The choice is motivated by notable similarities between ASP and FO(ID), even if both approaches trace back to different origins

Sign in / Sign up

Export Citation Format

Share Document