Guarded logic

Last updated

Guarded logic is a choice set of dynamic logic involved in choices, where outcomes are limited.

Contents

A simple example of guarded logic is as follows: if X is true, then Y, else Z can be expressed in dynamic logic as (X?;Y)∪(~X?;Z). This shows a guarded logical choice: if X holds, then X?;Y is equal to Y, and ~X?;Z is blocked, and Y∪block is also equal to Y. Hence, when X is true, the primary performer of the action can only take the Y branch, and when false the Z branch. [1]

A real-world example is the idea of paradox: something cannot be both true and false. A guarded logical choice is one where any change in true affects all decisions made down the line. [2]

History

Before the use of guarded logic there were two major terms used to interpret modal logic. Mathematical logic and database theory (Artificial Intelligence) were first-order predicate logic. Both terms found sub-classes of first-class logic and efficiently used in solvable languages which can be used for research. But neither could explain powerful fixed-point extensions to modal style logics.

Later Moshe Y. Vardi [3] made a conjecture that a tree model would work for many modal style logics. The guarded fragment of first-order logic was first introduced by Hajnal Andréka, István Németi and Johan van Benthem in their article Modal languages and bounded fragments of predicate logic. They successfully transferred key properties of description, modal, and temporal logic to predicate logic. It was found that the robust decidability of guarded logic could be generalized with a tree model property. The tree model can also be a strong indication that guarded logic extends modal framework which retains the basics of modal logics.

Modal logics are generally characterized by invariances under bisimulation. It also so happens that invariance under bisimulation is the root of tree model property which helps towards defining automata theory.

Types of guarded logic

Within Guarded Logic there exists numerous guarded objects. The first being guarded fragment which are first-order logic of modal logic. Guarded fragments generalize modal quantification through finding relative patterns of quantification. The syntax used to denote guarded fragment is GF. Another object is guarded fixed point logic denoted μGF naturally extends guarded fragment from fixed points of least to greatest. Guarded bisimulations are objects which when analyzing guarded logic. All relations in a slightly modified standard relational algebra with guarded bisimulation and first-order definable are known as guarded relational algebra. This is denoted using GRA.

Along with first-order guarded logic objects, there are objects of second-order guarded logic. It is known as Guarded Second-Order Logic and denoted GSO. Similar to second-order logic, guarded second-order logic quantifies whose range over guarded relations restrict it semantically. This is different from second-order logic which the range is restricted over arbitrary relations. [4]

Definitions of guarded logic

Let B be a relational structure with universe B and vocabulary τ.

i) A set X ⊆ B is guarded in B if there exists a ground atom α(b_1, ..., b_k) in B such that X = {b_1, ..., b_k}.

ii) A τ-structure A, in particular a substructure A ⊆ B, is guarded if its universe is a guarded set in A (in B).

iii) A tuple (b_1, ..., b_n) ∈ B^n is guarded in B if {b_1, ..., b_n} ⊆ X for some guarded set X ⊆ B.

iv) A tuple (b_1, ..., b_k) ∈ B^k is a guarded list in B if its components are pairwise distinct and {b_1, ..., b_k} is a guarded set. The empty list is taken to be a guarded list.

v) A relation X ⊆ B^n is guarded if it only consists of guarded tuples. [5]

Guarded bisimulation

A guarded bisimulation between two τ-structures A and B is a non-empty set I of finite partial isomorphic f: X → Y from A to B such that the back and forth conditions are satisfied.

Back: For every f: X → Y in I and for every guarded set Y` ⊆ B, there exists a partial isomorphic g: X` → Y` in I such that f^-1 and g^-1 agree on Y ∩ Y`.

Forth For every f: X → Y in I and for every guarded set X` ⊆ A, there exists a partial isomorphic g: X` → Y` in I such that f and g agree on X ∩ X`.

Related Research Articles

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

Original proof of Gödels completeness theorem

The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.

In mathematics, a finitary relation over sets X1, ..., Xn is a subset of the Cartesian product X1 × ⋯ × Xn; that is, it is a set of n-tuples (x1, ..., xn) consisting of elements xi in Xi. Typically, the relation describes a possible connection between the elements of an n-tuple. For example, the relation "x is divisible by y and z" consists of the set of 3-tuples such that when substituted to x, y and z, respectively, make the sentence true.

The relational model (RM) for database management is an approach to managing data using a structure and language consistent with first-order predicate logic, first described in 1969 by English computer scientist Edgar F. Codd, where all data is represented in terms of tuples, grouped into relations. A database organized in terms of the relational model is a relational database.

In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.

In the foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel-Choice set theory (ZFC). NBG introduces the notion of class, which is a collection of sets defined by a formula whose quantifiers range only over sets. NBG can define classes that are larger than sets, such as the class of all sets and the class of all ordinals. Morse–Kelley set theory (MK) allows classes to be defined by formulas whose quantifiers range over classes. NBG is finitely axiomatizable, while ZFC and MK are not.

In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL*, which additionally allows branching time and quantifiers. Subsequently, LTL is sometimes called propositional temporal logic, abbreviated PTL. In terms of expressive power, linear temporal logic (LTL) is a fragment of first-order logic.

Datalog is a declarative logic programming language that syntactically is a subset of Prolog. It is often used as a query language for deductive databases. In recent years, Datalog has found new application in data integration, information extraction, networking, program analysis, security, cloud computing and machine learning.

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic. For example, it can express branching quantifier sentences, such as the formula which expresses infinity in the empty signature; this cannot be done in FOL. Therefore, first-order logic cannot, in general, express this pattern of dependency, in which depends only on and , and depends only on and . IF logic is more general than branching quantifiers, for example in that it can express dependencies that are not transitive, such as in the quantifier prefix , which expresses that depends on , and depends on , but does not depend on .

In universal algebra and mathematical logic, a term algebra is a freely generated algebraic structure over a given signature. For example, in a signature consisting of a single binary operation, the term algebra over a set X of variables is exactly the free magma generated by X. Other synonyms for the notion include absolutely free algebra and anarchic algebra.

In mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic. Compound formulas are formed by combining the atomic formulas using the logical connectives.

In logic, a modal companion of a superintuitionistic (intermediate) logic L is a normal modal logic that interprets L by a certain canonical translation, described below. Modal companions share various properties of the original intermediate logic, which enables to study intermediate logics using tools developed for modal logic.

In descriptive complexity, a branch of computational complexity, FO is a complexity class of structures that can be recognized by formulas of first-order logic, and also equals the complexity class AC0. Descriptive complexity uses the formalism of logic, but does not use several key notions associated with logic such as proof theory or axiomatization.

In mathematical logic, a Lindström quantifier is a generalized polyadic quantifier. Lindström quantifiers generalize first-order quantifiers, such as the existential quantifier, the universal quantifier, and the counting quantifiers. They were introduced by Per Lindström in 1966. They were later studied for their applications in logic in computer science and database query languages.

In database theory, a conjunctive query is a restricted form of first-order queries using the logical conjunction operator. Many first-order queries can be written as conjunctive queries. In particular, a large part of queries issued on relational databases can be expressed in this way. Conjunctive queries also have a number of desirable theoretical properties that larger classes of queries do not share.

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation. The general study of interpretations of formal languages is called formal semantics.

In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of bounded treewidth. It is also of fundamental importance in automata theory, where the Büchi-Elgot-Trakhtenbrot theorem gives a logical characterization of the regular languages.

In logic, a quantifier is an operator that specifies how many individuals in the domain of discourse satisfy an open formula. For instance, the universal quantifier in the first order formula expresses that everything in the domain satisfies the property denoted by . On the other hand, the existential quantifier in the formula expresses that there is something in the domain which satisfies that property. A formula where a quantifier takes widest scope is called a quantified formula. A quantified formula must contain a bound variable and a subformula specifying a property of the referent of that variable.

In relational database theory, a tuple-generating dependency (TGD) is a certain kind of constraint on a relational database. It is a subclass of the class of embedded dependencies (EDs).

A tree stack automaton is a formalism considered in automata theory. It is a finite state automaton with the additional ability to manipulate a tree-shaped stack. It is an automaton with storage whose storage roughly resembles the configurations of a thread automaton. A restricted class of tree stack automata recognises exactly the languages generated by multiple context-free grammars.

References

  1. ↑ "Formal modeling and analysis of timed system". International Conference on Formal Modelling and Analysis of Timed Systems No4. Paris, France. September 25–27, 2006.
  2. ↑ Nieuwenhuis, Robert; Andrei Voronkov (2001). Logic for Programming, Artificial Intelligence, and Reasoning. Springer. pp.  88–89. ISBN   3-540-42957-3.
  3. ↑ Vardi, Moshe (1998). Reasoning about the Past with Two-Way Automata (PDF).
  4. ↑ "Guarded Logics: Algorithms and Bisimulation" (PDF). pp. 26–48. Retrieved 15 May 2014.
  5. ↑ "Guarded Logics: Algorithms and Bisimulation" (PDF). p. 25. Retrieved 15 May 2014.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.