The logic of definitions is a family of logics for encoding and reasoning about judgments, which are atomic predicates specified by inference rules. A definition associates an atomic predicate with a logical formula, which may itself depend on the predicate being defined. This leads to an apparent circularity which can be resolved by interpreting definitions as monotone fixed-point operators on terms, and which is enforced by imposing a stratification condition on definitions. In many instances, it is useful to consider definitions in which the predicate being defined appears negatively in the body of its definition. In the logic $\mathcal G$, underlying the Abella proof assistant, this is not allowed due to the stratification condition. One such application violating this condition is that of defining logical relations, which is a technique commonly used to prove properties about programming languages. Tiu has shown how to relax this stratification condition to allow for a broader body of definitions including that needed for logical relations. However, he only showed how to extend a core fragment of $\mathcal G$ with the weakened stratification condition, resulting in a logic he called $\mathrm{LD}$. In this work we show that the weakened stratification condition is also compatible with generic (nabla) quantification and general induction. The eventual aim of this work is to justify an extension of the Abella proof assistant allowing for such definitions.
We study the notion of stratification, as used in subsystems of linear logic with low complexity bounds on the cut-elimination procedure (the so-called light logics), from an abstract point of view, introducing a logical system in which stratification is handled by a separate modality. This modality, which is a generalization of the paragraph modality of Girard's light linear logic, arises from a general categorical construction applicable to all models of linear logic. We thus learn that stratification may be formulated independently of exponential modalities; when it is forced to be connecte…
An attempt at unifying logic and functional programming is reported. As a starting point, we take the view that "logic programs" are not about logic but constitute inductive definitions of sets and relations. A skeletal language design based on these considerations is sketched and a prototype implementation discussed.
Logic programming with fixed-point definitions is a useful extension of traditional logic programming. Fixed-point definitions can capture simple model checking problems and closed-world assumptions. Its operational semantics is typically based on intuitionistic provability. We extend the operational semantics of these languages with game semantics. This extended semantics has several interesting aspects: in particular, it gives a logical status to the $read$ predicate.
We derive a Prolog theorem prover for an Intuitionistic Epistemic Logic by starting from the sequent calculus {\bf G4IP} that we extend with operator definitions providing an embedding in intuitionistic propositional logic ({\bf IPC}). With help of a candidate definition formula generator, we discover epistemic operators for which axioms and theorems of Artemov and Protopopescu's {\em Intuitionistic Epistemic Logic} ({\bf IEL}) hold and formulas expected to be non-theorems fail. We compare the embedding of {\bf IEL} in {\bf IPC} with a similarly discovered successful embedding of Dosen's doubl…
We introduce fixpoint definitions, a rule-based reformulation of fixpoint constructs. The logic FO(FD), an extension of classical logic with fixpoint definitions, is defined. We illustrate the relation between FO(FD) and FO(ID), which is developed as an integration of two knowledge representation paradigms. The satisfiability problem for FO(FD) is investigated by first reducing FO(FD) to difference logic and then using solvers for difference logic. These reductions are evaluated in the computation of models for FO(FD) theories representing fairness conditions and we provide potential applicati…
We develop a doubly-exponential decision procedure for the satisfiability problem of guarded separation logic -- a novel fragment of separation logic featuring user-supplied inductive predicates, Boolean connectives, and separating connectives, including restricted (guarded) versions of negation, magic wand, and septraction. Moreover, we show that dropping the guards for any of the above connectives leads to an undecidable fragment. We further apply our decision procedure to reason about entailments in the popular symbolic heap fragment of separation logic. In particular, we obtain a doubly-ex…
The entailment between separation logic formulae with inductive predicates, also known as symbolic heaps, has been shown to be decidable for a large class of inductive definitions. Recently, a 2-EXPTIME algorithm was proposed and an EXPTIME-hard bound was established; however no precise lower bound is known. In this paper, we show that deciding entailment between predicate atoms is 2-EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines.
Predicate Logic with Definitions (PLD or D-logic) is a modification of first-order logic intended mostly for practical formalization of mathematics. The main syntactic constructs of D-logic are terms, formulas and definitions. A definition is a definition of variables, a definition of constants, or a composite definition (D-logic has also abbreviation definitions called abbreviations). Definitions can be used inside terms and formulas. This possibility alleviates introducing new quantifier-like names. Composite definitions allow constructing new definitions from existing ones.
In standard epistemic logic, knowing that p is the same as knowing that p is true, but it does not say anything about understanding p or knowing its meaning. In this paper, we present a conservative extension of Public Announcement Logic (PAL) in which agents have knowledge or belief about both the truth values and the meanings of propositions. We give a complete axiomatization of PAL with Boolean Definitions and discuss various examples. An agent may understand a proposition without knowing its truth value or the other way round. Moreover, multiple agents can agree on something without agreei…
The definition is a common form of human expert knowledge, a building block of formal science and mathematics, a foundation for database theory and is supported in various forms in many knowledge representation and formal specification languages and systems. This paper is a formal study of some of the most common forms of inductive definitions found in scientific text: monotone inductive definition, definition by induction over a well-founded order and iterated inductive definitions. We define a logic of definitions offering a uniform formal syntax to express definitions of the different sorts…
Classical logic is embedded into constructive logic, through a definition of the classical connectives and quantifiers in terms of the constructive ones.
Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of recursive specifications. These specifications are not directly complemented by fixed-point reasoning techniques and, correspondingly, do not have to satisfy strong monotonicity restrictions. We show how to incorporate a rewriting capability into logics of fixed-point definitions towards additionally supporting recursive specifications. In particular, we describe…
Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-ord…
Many semantical aspects of programming languages, such as their operational semantics and their type assignment calculi, are specified by describing appropriate proof systems. Recent research has identified two proof-theoretic features that allow direct, logic-based reasoning about such descriptions: the treatment of atomic judgments as fixed points (recursive definitions) and an encoding of binding constructs via generic judgments. However, the logics encompassing these two features have thus far treated them orthogonally: that is, they do not provide the ability to define object-logic proper…
The goal of this paper is to extend classical logic with a generalized notion of inductive definition supporting positive and negative induction, to investigate the properties of this logic, its relationships to other logics in the area of non-monotonic reasoning, logic programming and deductive databases, and to show its application for knowledge representation by giving a typology of definitional knowledge.
We show that the vast majority of extensions of the description logic $\mathcal{EL}$ do not enjoy the Craig interpolation nor the projective Beth definability property. This is the case, for example, for $\mathcal{EL}$ with nominals, $\mathcal{EL}$ with the universal role, $\mathcal{EL}$ with a role inclusion of the form $r\circ s\sqsubseteq s$, and for $\mathcal{ELI}$. It follows in particular that the existence of an explicit definition of a concept or individual name cannot be reduced to subsumption checking via implicit definability. We show that nevertheless the existence of interpolants …
There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification "every request is eventually followed by an acknowledgment" is satisfied vacuously by a system that never generates any requests. Vacuous satisfaction misleads users of model-checking into thinking that a system is correct. There are several existing definitions of vacuity. Originally, Beer et al. formalized vacuity as insensitivity to syntactic perturbation. However, this definition is only reasonable for vacuity in a single occurrence. Ar…
A proof procedure, in the spirit of the sequent calculus, is proposed to check the validity of entailments between Separation Logic formulas combining inductively defined predicates denoted structures of bounded tree width and theory reasoning. The calculus is sound and complete, in the sense that a sequent is valid iff it admits a (possibly infinite) proof tree. We show that the procedure terminates in the two following cases: (i) When the inductive rules that define the predicates occurring on the left-hand side of the entailment terminate, in which case the proof tree is always finite. (ii)…
A new criterion of comprehension is defined, initially termed by myself as "connected" and finally as "Acyclic" by Mr. Randall Holmes. Acyclic comprehension simply asserts that for any acyclic formula phi, the set {x:phi} exists. I first presented this criterion semi-formally to Mr. Randall Holmes, who further made the first rigorous definition of it, a definition that I finally simplified to the one presented here. Later Mr. Holmes made another presentation of the definition which is also mentioned here. He pointed to me that acyclic comprehension is implied by stratification, and posed the q…
There is a growing need for abstractions in logic specification languages such as FO(.) and ASP. One technique to achieve these abstractions are templates (sometimes called macros). While the semantics of templates are virtually always described through a syntactical rewriting scheme, we present an alternative view on templates as second order definitions. To extend the existing definition construct of FO(.) to second order, we introduce a powerful compositional framework for defining logics by modular integration of logic constructs specified as pairs of one syntactical and one semantical ind…
The logic FO(ID) uses ideas from the field of logic programming to extend first order logic with non-monotone inductive definitions. Such logic formally extends logic programming, abductive logic programming and datalog, and thus formalizes the view on these formalisms as logics of (generalized) inductive definitions. The goal of this paper is to study a deductive inference method for PC(ID), which is the propositional fragment of FO(ID). We introduce a formal proof system based on the sequent calculus (Gentzen-style deductive system) for this logic. As PC(ID) is an integration of classical pr…
We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard's seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratification, based on inducing levels in proof nets by means of indexes, which allows us to extend Girard's systems while keeping the same complexity properties. In particular, it turns out that Girard's syste…
Well-known principles of induction include monotone induction and different sorts of non-monotone induction such as inflationary induction, induction over well-founded sets and iterated induction. In this work, we define a logic formalizing induction over well-founded sets and monotone and iterated induction. Just as the principle of positive induction has been formalized in FO(LFP), and the principle of inflationary induction has been formalized in FO(IFP), this paper formalizes the principle of iterated induction in a new logic for Non-Monotone Inductive Definitions (ID-logic). The semantics…
Combining higher-order abstract syntax and (co)induction in a logical framework is well known to be problematic. Previous work described the implementation of a tool called Hybrid, within Isabelle HOL, which aims to address many of these difficulties. It allows object logics to be represented using higher-order abstract syntax, and reasoned about using tactical theorem proving and principles of (co)induction. In this paper we describe how to use it in a multi-level reasoning fashion, similar in spirit to other meta-logics such as Twelf. By explicitly referencing provability in a middle layer c…
Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles are based on a proof theoretic (rather than set-theoretic) notion of definition. Definitions are akin to logic programs, where the left and right rules for defined atoms allow one to view theories as "closed" or defining fixed points. The use of definitions and free equality makes it possible to reason intentionally about syntax. We add in a consistent way …
Whereas standard treatments of temporal logic are adequate for closed systems, having no run-time interactions with their environment, they fall short for reactive systems, interacting with their environments through synchronisation of actions. This paper introduces reactive temporal logic, a form of temporal logic adapted for the study of reactive systems. I illustrate its use by applying it to formulate definitions of a fair scheduler, and of a correct mutual exclusion protocol. Previous definitions of these concepts were conceptually much more involved or less precise, leading to debates on…
Logic can be made useful for programming and for databases independently of logic programming. To be useful in this way, logic has to provide a mechanism for the definition of new functions and new relations on the basis of those given in the interpretation of a logical theory. We provide this mechanism by creating a compositional semantics on top of the classical semantics. In this approach verification of computational results relies on a correspondence between logic interpretations and a class definition in languages like Java or C++. The advantage of this approach is the combination of an …
The entailment problem $φ\models ψ$ in Separation Logic \cite{IshtiaqOHearn01,Reynolds02}, between separated conjunctions of equational ($x \iseq y$ and $x \not\iseq y$), spatial ($x \mapsto (y_1,\ldots,y_\rank)$) and predicate ($p(x_1,\ldots,x_n)$) atoms, interpreted by a finite set of inductive rules, is undecidable in general. Certain restrictions on the set of inductive definitions lead to decidable classes of entailment problems. Currently, there are two such decidable classes, based on two restrictions, called \emph{establishment} \cite{IosifRogalewiczSimacek13,KatelaanMathejaZuleger19,P…
The set of integer number lists with finite length, and the set of binary trees with integer labels are both countably infinite. Many inductively defined types also have countably many elements. In this paper, we formalize the syntax of first order inductive definitions in Coq and prove them countable, under some side conditions. Instead of writing a proof generator in a meta language, we develop an axiom-free proof in the Coq object logic. In other words, our proof is a dependently typed Coq function from the syntax of the inductive definition to the countability of the type. Based on this pr…
We present alternative definitions of the first-order stable model semantics and its extension to incorporate generalized quantifiers by referring to the familiar notion of a reduct instead of referring to the SM operator in the original definitions. Also, we extend the FLP stable model semantics to allow generalized quantifiers by referring to an operator that is similar to the $\sm$ operator. For a reasonable syntactic class of logic programs, we show that the two stable model semantics of generalized quantifiers are interchangeable.
Distributed Autoepistemic Logic with Inductive Definitions (dAEL(ID)) is a recently proposed non-monotonic logic for says-based access control. We define a query-driven decision procedure for dAEL(ID) that is implemented in the knowledge-base system IDP. The decision procedure is designed in such a way that it allows one to determine access rights while avoiding redundant information flow between principals in order to enhance security and reduce privacy concerns. Given that the decision procedure has in the worst case an exponential runtime, it is to be regarded as a proof of concept that inc…
In logics with the Craig interpolation property (CIP) the existence of an interpolant for an implication follows from the validity of the implication. In logics with the projective Beth definability property (PBDP), the existence of an explicit definition of a relation follows from the validity of a formula expressing its implicit definability. The two-variable fragment, FO2, and the guarded fragment, GF, of first-order logic both fail to have the CIP and the PBDP. We show that nevertheless in both fragments the existence of interpolants and explicit definitions is decidable. In GF, both probl…
The logic of information flows (LIF) is a general framework in which tasks of a procedural nature can be modeled in a declarative, logic-based fashion. The first contribution of this paper is to propose semantic and syntactic definitions of inputs and outputs of LIF expressions. We study how the two relate and show that our syntactic definition is optimal in a sense that is made precise. The second contribution is a systematic study of the expressive power of sequential composition in LIF. Our results on composition tie in the results on inputs and outputs, and relate LIF to first-order logic …
We discuss four common mistakes in the teaching and textbooks of modal logic. The first one is missing the axiom $\Diamondφ\leftrightarrow\neg\Box\negφ$, when choosing $\Diamond$ as the primitive modal operator, misunderstanding that $\Box$ and $\Diamond$ are symmetric. The second one is forgetting to make the set of formulas for filtration closed under subformulas, when proving the finite model property through filtration, neglecting that $\Boxφ$ and $\Diamondφ$ may be abbreviations of formulas. The third one is giving wrong definitions of canonical relations in minimal canonical models that …
Lambda Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an encoding that maps both terms and types of the object logic (higher-order logic) to terms of the metalanguage (Lambda Prolog). We discuss both the Terzo and Teyjus implementations of Lambda Prolog. We also encode the same logic in Twelf and compare the features of these two metalanguages for our purposes.
Girard's Light linear logic (LLL) characterized polynomial time in the proof-as-program paradigm with a bound on cut elimination. This logic relied on a stratification principle and a "one-door" principle which were generalized later respectively in the systems L^4 and L^3a. Each system was brought with its own complex proof of Ptime soundness. In this paper we propose a broad sufficient criterion for Ptime soundness for linear logic subsystems, based on the study of paths inside the proof-nets, which factorizes proofs of soundness of existing systems and may be used for future systems. As an …
Constraint propagation is one of the basic forms of inference in many logic-based reasoning systems. In this paper, we investigate constraint propagation for first-order logic (FO), a suitable language to express a wide variety of constraints. We present an algorithm with polynomial-time data complexity for constraint propagation in the context of an FO theory and a finite structure. We show that constraint propagation in this manner can be represented by a datalog program and that the algorithm can be executed symbolically, i.e., independently of a structure. Next, we extend the algorithm to …
Complex vector analysis is widely used to analyze continuous systems in many disciplines, including physics and engineering. In this paper, we present a higher-order-logic formalization of the complex vector space to facilitate conducting this analysis within the sound core of a theorem prover: HOL Light. Our definition of complex vector builds upon the definitions of complex numbers and real vectors. This extension allows us to extensively benefit from the already verified theorems based on complex analysis and real vector analysis. To show the practical usefulness of our library we adopt it …
Separation Logic is a widely used formalism for describing dynamically allocated linked data structures, such as lists, trees, etc. The decidability status of various fragments of the logic constitutes a long standing open problem. Current results report on techniques to decide satisfiability and validity of entailments for Separation Logic(s) over lists (possibly with data). In this paper we establish a more general decidability result. We prove that any Separation Logic formula using rather general recursively defined predicates is decidable for satisfiability, and moreover, entailments betw…
This paper provides an abstract definition of some kinds of logics, called diagrammatic logics, together with a definition of morphisms and of 2-morphisms between diagrammatic logics. The definition of the 2-category of diagrammatic logics rely on category theory, mainly on adjunction, categories of fractions and limit sketches. This framework is applied to the formalization of a parameterization process. This process, which consists in adding a formal parameter to some operations in a given specification, is presented as a morphism of logics. Then the parameter passing process, for recovering…
Separation Logic with inductive definitions is a well-known approach for deductive verification of programs that manipulate dynamic data structures. Deciding verification conditions in this context is usually based on user-provided lemmas relating the inductive definitions. We propose a novel approach for generating these lemmas automatically which is based on simple syntactic criteria and deterministic strategies for applying them. Our approach focuses on iterative programs, although it can be applied to recursive programs as well, and specifications that describe not only the shape of the da…
We define a class of Separation Logic formulae, whose entailment problem: given formulae $ϕ, ψ_1, \ldots, ψ_n$, is every model of $ϕ$ a model of some $ψ_i$? is 2EXPTIME-complete. The formulae in this class are existentially quantified separating conjunctions involving predicate atoms, interpreted by the least sets of store-heap structures that satisfy a set of inductive rules, which is also part of the input to the entailment problem. Previous work consider established sets of rules, meaning that every existentially quantified variable in a rule must eventually be bound to an allocated locatio…
In this paper we adapt the definitions and results from Apt and Vermeulen on `First order logic as a constraint programming language' (in: Proceedings of LPAR2001, Baaz and Voronkov (eds.), Springer LNAI 2514) to include important ideas about search and choice into the system. We give motivating examples. Then we set up denotational semantics for first order logic as follows: the semantic universe includes states that consist of two components: a substitution, which can be seen as the computed answer; and a constraint satisfaction problem, which can be seen as the residue of the original probl…
Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such descriptions: the interpretation of atomic judgments through recursive definitions and an encoding of binding constructs via generic judgments. However, logics encompassing these two features do not currently allow for the definition of relations that embody dynamic aspects related to binding, a capability needed in many reasoning tasks. We propose a new relation betw…
Prime implicates and prime implicants have proven relevant to a number of areas of artificial intelligence, most notably abductive reasoning and knowledge compilation. The purpose of this paper is to examine how these notions might be appropriately extended from propositional logic to the modal logic K. We begin the paper by considering a number of potential definitions of clauses and terms for K. The different definitions are evaluated with respect to a set of syntactic, semantic, and complexity-theoretic properties characteristic of the propositional definition. We then compare the definitio…
Higher-order logic programming is an interesting extension of traditional logic programming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higher-order characteristics are indeed desirable but on the other hand they are also usually more expensive to support. In this paper we propose a program specialization technique based on partial evaluation that can be applied to a modest but useful class of higher-order logic programs and can transform them into first-order programs without introducing additional data structures. The resulting fir…
Weak affine light typing (WALT) assigns light affine linear formulae as types to a subset of lambda-terms in System F. WALT is poly-time sound: if a lambda-term M has type in WALT, M can be evaluated with a polynomial cost in the dimension of the derivation that gives it a type. In particular, the evaluation can proceed under any strategy of a rewriting relation, obtained as a mix of both call-by-name/call-by-value beta-reductions. WALT is poly-time complete since it can represent any poly-time Turing machine. WALT weakens, namely generalizes, the notion of stratification of deductions common …
Previous research into the relation between ASP and classical logic has identified at least two different ways in which the former extends the latter. First, ASP program typically contain sets of rules that can be naturally interpreted as inductive definitions, and the language FO(ID) has shown that such inductive definitions can elegantly be added to classical logic in a modular way. Second, there is of course also the well-known epistemic component of ASP, which was mainly emphasized in the early papers on stable model semantics. To investigate whether this kind of knowledge can also, and in…
Logical frameworks are meta-formalisms in which the syntax and semantics of object logics and related formal systems can be defined. This allows object logics to inherit implementations from the framework including, e.g., parser, type checker, or module system. But if the desired object logic falls outside the comfort zone of the logical framework, these definitions may become cumbersome or infeasible. Therefore, the MMT system abstracts even further than previous frameworks: it assumes no type system or logic at all and allows its kernel algorithms to be customized by almost arbitrary sets of…
