Uncertain deductive databases: A hybrid approach

Uncertainty in deductive databases and logic programming has been modeled using a variety of (numeric and non-numeric) formalisms in the past, including probabilistic, possibilistic, and fuzzy set-theoretic approaches, and many valued logic programming. In this paper, we consider a hybrid approach to the modeling of uncertainty in deductive databases. Our model, called deductive IST (DIST) is based on an extension of the Information Source Tracking (IST) model, recently proposed for relational databases. The DIST model permits uncertainty to be modeled and manipulated in essentially qualitative terms with an option to convert qualitative expressions of uncertainty into numeric form (e.g., probabilities). An uncertain deductive database is modeled as a Horn clause program in the DIST framework, where each fact and rule is annotated with an expression indicating the “sources” contributing to this information and their nature of contribution. (1) We show that positive DIST programs enjoy the least model/least fixpoint semantics analogous to classical logic programs. (2) We show that top-down (e.g., SLD-resolution) and bottom-up (e.g., magic sets rewriting followed by semi-naive evaluation) query processing strategies developed for datalog can be easily extended to DIST programs. (3) Results and techniques for handling negation as failure in classical logic programming can be easily extended to DIST. As an illustration of this, we show how stratified negation can be so extended. We next study the problem of query optimization in such databases and establish the following results. (4) We formulate query containment in qualitative as well as quantitative terms. Intuitively, our qualitative sense of containment would say a query Q₁ is contained in a query Q₂ provided for every input database D, for every tuple t, t ε Q₂(D) holds in every “situation” in which t ε Q₁(D) is true. The quantitative notion of containment would say Q₁ is contained in Q₂ provided on every input, the certainty associated with any tuple computed by Q₁ is no more than the certainty associated with the same tuple by Q₂ on the given input. We also prove that qualitative and quantitative notions of containment (both absolute and uniform versions) coincide. (5) We establish necessary and sufficient conditions for the qualitative containment of conjunctive queries. (6) We extend the well-known chase technique to develop a test for uniform containment and equivalence of positive DIST programs. (7) Finally, we prove that the complexity of testing containment of conjunctive DIST queries remains the same as in the classical case when number of information sources is regarded as a constant (so, it's NP-complete in the size of the queries). We also show that testing containment of conjunctive queries is co-NP-complete in the number of information sources.     

Constructive logics Part I: A tutorial on proof systems and typed λ-calculi

The purpose of this paper is to give an exposition of material dealing with constructive logics, typed λ-calculi, and linear logic. The emergence in the past ten years of a coherent field of research often named “logic and computation” has had two major (and related) effects: firstly, it has rocked vigorously the world of mathematical logic; secondly, it has created a new computer science discipline, which spans a range of subjects from what is traditionally called the theory of computation, to programming language design. Remarkably, this new body of work relies heavily on some “old” concepts found in mathematical logic, like natural deduction, sequent calculus, and λ-calculus (but often viewed in a different light), and also on some newer concepts. Thus, it may be quite a challenge to become initiated to this new body of work (but the situation is improving, and there are now some excellent texts on this subject matter). This paper attempts to provide a coherent and hopefully “gentle” initiation to this new body of work. We have attempted to cover the basic material on natural deduction, sequent calculus, and typed λ-calculus, but also to provide an introduction to Girard's linear logic, one of the most exciting developments in logic these past six years. The first part of these notes gives an exposition of the background material (with some exceptions, such as “contraction-free” systems for intuitionistic propositional logic and the Girard translation of classical logic into intuitionistic logic, which is new). The second part is devoted to more current topics such as linear logic, proof nets, the geometry of interaction, and unified systems of logic (LU).     

Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification

We characterize provability in intuitionistic logic with equality in terms of a constraint calculus. This characterization uncovers close connections between provability in intuitionistic logic with equality and solutions to simultaneous rigid E-unification. We show that the problem of existence of a sequent proof with a given skeleton is polynomial-time equivalent to simultaneous rigid E-unifiability. This gives us a proof procedure for intuitionistic logic with equality modulo simultaneous rigid E-unification. We also show that simultaneous rigid E-unifiability is polynomial-time reducible to intuitionistic logic with equality. Thus, any proof procedure for intuitionistic logic with equality can be considered as a procedure for simultaneous rigid E-unifiability. In turn, any procedure for simultaneous rigid E-unifiability gives a procedure for establishing provability in intuitionistic logic with equality.     

Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification

We characterize provability in intuitionistic logic with equality in terms of a constraint calculus. This characterization uncovers close connections between provability in intuitionistic logic with equality and solutions to simultaneous rigid E-unification. We show that the problem of existence of a sequent proof with a given skeleton is polynomial-time equivalent to simultaneous rigid E-unifiability. This gives us a proof procedure for intuitionistic logic with equality modulo simultaneous rigid E-unification. We also show that simultaneous rigid E-unifiability is polynomial-time reducible to intuitionistic logic with equality. Thus, any proof procedure for intuitionistic logic with equality can be considered as a procedure for simultaneous rigid E-unifiability. In turn, any procedure for simultaneous rigid E-unifiability gives a procedure for establishing provability in intuitionistic logic with equality.     

Uniform provability realization of intuitionistic logic, modality and λ-terms

The intended meaning of intuitionistic logic is explained by the Brouwer-Heyting-Kolmogorov (BHK) provability semantics which informally defines intuitionistic truth as provability and specifies the intuitionistic connectives via operations on proofs. The problem of finding an adequate formalization of the provability semantics and establishing the completeness of the intuitionistic logic Int was first raised by Gödel in 1933. This question turned out to be a part of the more general problem of the intended realization for Gödel's modal logic of provability S4 which was open since 1933. In this tutorial talk we present a provability realization of Int and S4 that solves both of these problems. We describe the logic of explicit provability (LP) with the atoms “t is a proof of F” and establish that every theorem of S4 admits a reading in LP as the statement about operations on proofs. Moreover, both S4 and Int are shown to be complete with respect to this realization. In addition, LP subsumes the λ-calculus, modal λ-calculus, combinatory logic and provides a uniform provability realization of modality and λ-terms.     

Semantic forgetting in answer set programming

The notion of forgetting, also known as variable elimination, has been investigated extensively in the context of classical logic, but less so in (nonmonotonic) logic programming and nonmonotonic reasoning. The few approaches that exist are based on syntactic modifications of a program at hand. In this paper, we establish a declarative theory of forgetting for disjunctive logic programs under answer set semantics that is fully based on semantic grounds. The suitability of this theory is justified by a number of desirable properties. In particular, one of our results shows that our notion of forgetting can be entirely captured by classical forgetting. We present several algorithms for computing a representation of the result of forgetting, and provide a characterization of the computational complexity of reasoning from a logic program under forgetting. As applications of our approach, we present a fairly general framework for resolving conflicts in inconsistent knowledge bases that are represented by disjunctive logic programs, and we show how the semantics of inheritance logic programs and update logic programs from the literature can be characterized through forgetting. The basic idea of the conflict resolution framework is to weaken the preferences of each agent by forgetting certain knowledge that causes inconsistency. In particular, we show how to use the notion of forgetting to provide an elegant solution for preference elicitation in disjunctive logic programming.     

Focusing and polarization in linear,intuitionistic, and classical logics

A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. These focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system LKF for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard’s LC and LU proof systems.     

Declarative paradigm of test coverage

Two facts about declarative programming prevent the application of conventional testing methods. First, the classical test coverage measures such as statement, branch or path coverage, cannot be used, since in declarative programs no control flow notion exists. Second, there is no widely accepted language available for formal specification, since predicate logic, which is the most common formalism for declarative programming, is already a very high-level abstract language. This paper presents a new approach exending previous work by the authors on test input generation for declarative programs. For this purpose, the existing program instrumentation notion is extended and a new logic coverage measure is introduced. The approach is mathematically formalized and the goal of achieving 100% program logic coverage controls the automatic test input generation. The method is depicted by means of logic programming; the results are, however, generally applicable. Finally, the concepts introduced have been used practically within a test environment. © 1998 John Wiley & Sons, Ltd.     

Arguments and Misunderstandings: Fuzzy Unification for Negotiating Agents

In this paper, we develop the notion of fuzzy unification and incorporate it into a novel fuzzy argumentation framework for extended logic programming. We make the following contributions: The argumentation framework is defined by a declarative bottom-up fixpoint semantics and an equivalent goal-directed top-down proofprocedure for extended logic programming. Our framework allows one to represent positive and explicitly negative knowledge, as well as uncertainty. Both concepts are used in agent communication languages such as KQML and FIPA ACL. One source of uncertainty in open systems stems from mismatches in parameter and predicate names and missing parameters. To this end, we conservatively extend classical unification and develop fuzzy unification based on normalised edit distance over trees.     

A new framework for declarative programming

We propose a new framework for the syntax and semantics of Weak Hereditarily Harrop logic programming with constraints, based on resolution over τ-categories: finite product categories with canonical structure.

Constraint information is directly built-in to the notion of signature via categorical syntax. Many-sorted equational are a special case of the formalism which combines features of uniform logic programming languages (moduels and hypothetical implication) with those of constraint logic programming. Using the cannoical structure supplied by τ-categories, we define a diagrammatic generalization of formulas, goals, programs and resolution proofs up to equality (rather than just up to isomorphism).

We extend the Kowalski-van Emden fixed point interpretation, a cornerstone of declarative semantics, to an operational, non-ground, categorical semantics based on indexing over sorts and programs.

We also introduce a topos-theoretic declarative semantics and show soundness and completeness of resolution proofs and of a sequent calculus over the categorical signature. We conclude with a discussion of semantic perspectives on uniform logic programming.     

A proof–theoretic study of the correspondence of hybrid logic and classical logic

In this paper, we show the equivalence between the provability of a proof system of basic hybrid logic and that of translated formulas of the classical predicate logic with equality and explicit substitution by a purely proof–theoretic method. Then we show the equivalence of two groups of proof systems of hybrid logic: the group of labelled deduction systems and the group of modal logic-based systems.     

Algorithmic Debugging and Hypothetical Reasoning

This paper presents a generalization of Shapiro style algorithmic debugging for generalized Horn clause intuitionistic logic. This logic offers hypothetical reasoning and negation is defined not by failure but by inconsistency. We extend Shapiro's notion of intended interpretation, symptoms and errors and give formal results paralleling those known for definite clauses. We also show how a corresponding diagnosis module for RISC- a logic programming system for generalized Horn clause intuitionistic logic-can be defined by meta interpretation. In contrast to Shapiro's PROLOG modules ours work independently of the specific computation rule that in RISC may be specified by the user.     

Rush Hour is PSPACE-complete, or “Why you should generously tip parking lot attendants”

Rush Hour is a children's game that consists of a grid board, several cars that are restricted to move either vertically or horizontally (but not both), a special target car, and a single exit on the perimeter of the grid. The goal of the game is to find a sequence of legal moves that allows the target car to exit the grid. We consider a slightly generalized version of the game that uses an n×n grid and assume that we can place the single exit and target car at any location we choose on initialization of the game.

In this work, we show that deciding if the target car can legally exit the grid is PSPACE-complete. Our constructive proof uses a lazy form of dual-rail reversible logic such that movement of “output” cars can only occur if logical combinations of “input” cars can also move. Emulating this logic only requires three types of devices (two switches and one crossover); thus, our proof technique can be easily generalized to other games and planning problems in which the same three primitive devices can be constructed.     

An Institutional View on Categorical Logic

We introduce a generic notion of categorical propositional logic and provide a construction of a preorder-enriched institution out of such a logic, following the Curry-Howard-Tait paradigm. The logics are speci ed as theories of a meta-logic within the logical framework LF such that institution comorphisms are obtained from theory morphisms of the meta-logic. We prove several logic-independent results including soundness and completeness theorems and instantiate our framework with a number of examples: classical, intuitionistic,linear and modal propositional logic.     

Semantical analysis of specification logic

The “specification logic” of J. C. Reynolds is a partial-correctness logic for Algol 60-like languages with procedures. It is interpreted here as an intuitionistic theory, using a form of possible-world semantics first applied to programming language interpretation by J. C. Reynolds and F. J. Oles to give an abstract treatment of stack-oriented storage management. The model provides a satisfactory solution to all previously known problems with the interpretation of specification logic; however, unexpected new problems have been discovered in doing this work, and these remain unsolved.     

Compiler Optimization Correctness by Temporal Logic

Rewrite rules with side conditions can elegantly express many classical compiler optimizations for imperative programming languages. In this paper, programs are written in an intermediate language and transformation-enabling side conditions are specified in a temporal logic suitable for describing program data flow.The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by three familiar optimizations: dead code elimination, constant folding, and code motion. A transformation is correct if whenever it can be applied to a program, the original and transformed programs are semantically equivalent, i.e., they compute the same input-output function. The proofs of semantic equivalence inductively show that a transformation-specific bisimulation relation holds between the original and transformed program computations.     

Intuitionistic hybrid logic: Introduction and survey

Intuitionistic hybrid logic is hybrid modal logic over an intuitionistic logic basis instead of a classical logical basis. In this short paper we introduce intuitionistic hybrid logic and we give a survey of work in the area.     

Timing Analysis of Combinational Circuits in Intuitionistic Propositional Logic

Classical logic has so far been the logic of choice in formal hardware verification. This paper proposes the application of intuitionistic logic to the timing analysis of digital circuits. The intuitionistic setting serves two purposes. The model-theoretic properties are exploited to handle the second-order nature of bounded delays in a purely propositional setting without need to introduce explicit time and temporal operators. The proof-theoretic properties are exploited to extract quantitative timing information and to reintroduce explicit time in a convenient and systematic way.We present a natural Kripke-style semantics for intuitionistic propositional logic, as a special case of a Kripke constraint model for Propositional Lax Logic (Information and Computation, Vol. 137, No. 1, 1–33, 1997), in which validity is validity up to stabilisation, and implication comes out as boundedly gives rise to. We show that this semantics is equivalently characterised by a notion of realisability with stabilisation bounds as realisers. Following this second point of view an intensional semantics for proofs is presented which allows us effectively to compute quantitative stabilisation bounds.We discuss the application of the theory to the timing analysis of combinational circuits. To test our ideas we have implemented an experimental prototype tool and run several examples.     

The Knower Paradox in the light of provability interpretations of modal logic

This paper propounds a systematic examination of the link between the Knower Paradox and provability interpretations of modal logic. The aim of the paper is threefold: to give a streamlined presentation of the Knower Paradox and related results; to clarify the notion of a syntactical treatment of modalities; finally, to discuss the kind of solution that modal provability logic provides to the Paradox. I discuss the respective strength of different versions of the Knower Paradox, both in the framework of first-order arithmetic and in that of modal logic with fixed point operators. It is shown that the notion of a syntactical treatment of modalities is ambiguous between a self-referential treatment and a metalinguistic treatment of modalities, and that these two notions are independent. I survey and compare the provability interpretations of modality respectively given by Skyrms, B. (1978, The Journal of Philosophy 75: 368–387) Anderson, C.A. (1983, The Journal of Philosophy 80: 338–355) and Solovay, R. (1976, Israel Journal of Mathematics 25: 287–304). I examine how these interpretations enable us to bypass the limitations imposed by the Knower Paradox while preserving the laws of classical logic, each time by appeal to a distinct form of hierarchy.