Gaggles, Gentzen and Galois: A Proof Theory for Algebraizable Logics
- Rajeev Goré
We show how the Gaggle Theory of Dunn gives a Gentzen-style proof theory for many algebraizable logics via the Display Logic of Belnap. At the heart of both systems lie the algebraic notions of residuation, Galois connections, and their duals. Introduction It is well known that most non-classical logics have an underlying algebraic semantics. Many non-classical logics also have a relational semantics using Kripke models. In a series of papers [Dun91, Dun93b, Dun93a], Dunn has shown that there are deep connections between these algebraic and relational semantics where each n-ary connective in a logic has an n + 1-ary relational...
A formalization of the Ramified Type Theory
- Twan Laan
In "Principia Mathematica " , B. Russell and A.N. Whitehead propose a type system for higher order logic. This system has become known under the name "ramified type theory". It was invented to avoid the paradoxes, which could be conducted from Frege's "Begriffschrift" . We give a formalization of the ramified type theory as described in the Principia Mathematica, trying to keep it as close as possible to the ideas of the Principia. As an alternative, distancing ourselves from the Principia, we express notions from the ramified type theory in a lambda calculus style, thus clarifying the type system of...
- Matthias Fuchs; Fachbereich Informatik
One of the many abilities that distinguish a mathematician from an automated deduction system is to be able to offer appropriate expressions based on intuition and experience that are substituted for existentially quantified variables so as to simplify the problem at hand substantially. We propose to simulate this ability with a technique called genetic programming for use in automated deduction. We apply this approach to problems of combinatory logic. Our experimental results show that the approach is viable and actually produces very promising results. A comparison with the renowned theorem prover Otter underlines the achievements. This work was supported by...
Chain Queries Expressible by Linear Datalog Programs
- Foto Afrati; Francesca Toni
We study the linearisability of chain queries and identify a new class of linearisable chain queries, referred to as pseudo-regular. We prove linearisability constructively, by generating, for any given pseudo-regular chain query, the Datalog program corresponding to it. 1 Introduction First-order (algebraic) query languages lack recursion and, as a consequence, have limited expressive power. Datalog, the language of Horn logic without function symbols, embeds recursion and therefore allows to express a far wider class of queries. However, queries expressed in Datalog are harder to evaluate than classical first-order queries. As a consequence, in the (deductive) database community, many efforts have...
THE TENTH WHITE HOUSE PAPERS Graduate Research in Cognitive and Computing Sciences at Sussex
- John C. Halbran; Fabrice P. Retkowsky (Eds.); John C. Halloran; Fabrice P. Retkowsky; Fabrice P. Retkowsky; Ahti Pietarinen
Defeasible Prolog is a Prolog metainterpreter designed by Nute to implement nonmonotonic inference based on a defeasible logic. In this paper it is first shown how to give proof conditions for even-if conditions of Nute's defeasible logic that allow also the preemption of defeaters. These conditions are then implemented to the defeasible Prolog. Finally, some computational results are presented for the given examples. 1 Introduction In Nute's defeasible reasoning (Nute, 1992, 1994a, 1994b), the main target is to give a formalised account of nonmonotonic defeasible inferences like "typically, j's are y", "normally, j's are y" or "usually, j's are y"....
On the Efficiency of Learning Techniques for Combinational Equivalence Checking
- C.A.J. van Eijk; G. L. J. M. Janssen
Recursive learning is a general technique for analyzing Boolean problems. In this paper, we evaluate various heuristics for improving the runtime efficiency of this technique when applied to the problem of combinational equivalence checking. All heuristics are evaluated on a set of 29 examples containing the ISCAS benchmarks as well as industrial designs. 1. Introduction In this paper we consider the problem of verifying the functional equivalence of combinational circuits in a logic synthesis environment. It is well known that to efficiently solve this problem, it is important to utilize the structural similarities that exist between the circuits preceding and...
Higher-Order Conditional Term Rewriting in the L lambda Logic Programming Language
- Amy Felty
In this paper, we extend the notions of first-order conditional rewrite systems and higher-order rewrite systems to obtain higher-order conditional rewriting. Such rewrite systems can be used to directly express many operations in theorem proving and functional programming. We then illustrate that these rewrite systems can be naturally specified and implemented in a higher-order logic programming language. This paper was presented at the Third International Workshop on Extensions of Logic Programming, February 1992. 1 Introduction Higher-order rewrite systems extend first-order rewrite systems and provide a mechanism for reasoning about equality in languages that include notions of bound variables [1, 9,...
Improvements in Program Synthesis Using Fine-Grain Sorted Logic
- Jochen Burghardt
: This paper introduces a new constructor-based sort discipline on predicate logic which allows to express more sophisticated sorts than conventional approaches. Algorithms are given to calculate infimum and difference of two sorts and to decide the subsort and the equivalence property. The range sort of a defined function is calculated from its defining equations, leading to a more exact description than obtaining a signature from the user: different equations are usually assigned different sorts. Thus, the sort discipline helps to select the "right" equations for inference steps, and cuts down the search space of a formal proof. This effect...
Guarded Fixed Point Logic
- Erich Grädel; Igor Walukiewicz
Guarded fixed point logics are obtained by adding least and greatest fixed points to the guarded fragments of firstorder logic that were recently introduced by Andréka, van Benthem and N emeti. Guarded fixed point logics can also be viewed as the natural common extensions of the modal µ-calculus and the guarded fragments. We prove that the satisfiability problems for guarded fixed point logics are decidable and complete for deterministic double exponential time. For guarded fixed point sentences of bounded width, the most important case for applications, the satisfiability problem is EXPTIME-complete.
Model-Based Diagnosis with Constraint Logic Programs
- Igor Mozetic; Christian Holzbaur
Model-based diagnosis is the activity of locating malfunctioning components of a system solely on the basis of its structure and behavior. In the paper we describe the role of Constraint Logic Programming (CLP) in representing models and the search space of minimal diagnoses. In particular, we concentrate on two instances of the CLP scheme: CLP(B) and CLP(!). CLP(B) extends the standard computational domain of logic programs by boolean expressions, while CLP(!) comprises a solver for systems of linear equations and inequalities over real-valued variables. 1 Introduction There are two fundamentaly different approaches to diagnostic reasoning. In the first, heuristic approach,...
A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs
- Amy Felty
In this paper, we show that an intuitionistic logic with second-order function quantification, called hh 2 here, can serve as a meta-language to directly and naturally specify both sequent calculi and natural deduction inference systems for first-order logic. For the intuitionistic subset of first-order logic, we present a set of hh 2 formulas which simultaneously specifies both kinds of inference systems and provides a direct and concise account of the correspondence between cut-free sequential proofs and normal natural deduction proofs. The logic of hh 2 can be implemented using such logic programming techniques as providing operational interpretations to the connectives...
Representing Incomplete Knowledge in Abductive Logic Programming
- Marc Denecker; Danny De Schreye
Recently, Gelfond and Lifschitz presented a formal language for representing incomplete knowledge on actions and states, and a sound translation from this language to extended logic programming. We present an alternative translation to abductive logic programming with integrity constraints and prove the soundness and completeness. In addition, we show how an abductive procedure can be used, not only for explanation, but also for deduction and proving satisfiability under uncertainty. From a more general perspective, this work can be viewed as a -successful- experiment in the declarative representation of and automated reasoning on incomplete knowledge using abductive logic programming.
Spatial Decision Making Based on Fuzzy Methodologies
- Emmanuel Stefanakis; Michael Vazirgiannis; Timos Sellis
At present, Geographic Information Systems (GIS) though powerful toolboxes, most with hundreds of functions, they suffer from several limitations which render them inefficient tools for spatial decision-making. This paper focuses on the inappropriate logical foundation incorporated into them and examines the necessity of adopting fuzzy logic methodologies in GIS operations. 1 INTRODUCTION Geographic Information Systems (GIS) are computer-based systems designed to support the capture, management, manipulation, analysis, modeling and display of spatially referenced data at different points in time [Aronoff, 1989]. Today, GISs are widely used in many government, business and private activities; which fall into three major categories [Maguire...
Generalised Unification of Temporal Logic Formulas
- Scott Hazelhurst
Given two temporal logic formulas, g and h, we wish to know whether there is a modification, m, we can make to h so that g =) h. This problem has important applications in hardware verification, where finding such modifications efficiently is important for an inferencing system. The temporal logic used, TL, is a relatively simple logic which is interpreted over finite state machine models. The modifications allowed are `time-shifting' (nesting under the next-time temporal operator) and substitution of expressions for variables. An algorithm has been developed and implemented in the Voss verification system. The basis of the algorithm is...
Tabulation of Automata for Tree Adjoining Languages
- Miguel A. Alonso Pardo; David Cabrero Souto; Eric de la Clergerie
We try to provide a common framework to clarify the relationships between dierent automata and their associated tabulation techniques for Tree Adjoning Languages, a subclass of Mildly Context-Sensitive Languages. We have chosen Logic Push-down Automata working with Linear Indexed Grammars as a starting point. Several tabulation techniques for dierent parsing strategies are proposed and compared with previous approaches. 1 Introduction The class of Mildly Context-Sensitive Languages (MCSL) is placed between context-free languages and context-sensitive languages. An important subclass in MCSL is that of Tree Adjoining Languages, which can be described by several grammar formalisms which have been shown to be...
The Knowledge Acquisition and Representation Language KARL
- Dieter Fensel; Jürgen Angele; Rudi Studer
The Knowledge Acquisition and Representation Language (KARL) combines a description of a knowledge-based system at the conceptual level (a so-called model of expertise) with a description at a formal and executable level. Thus, KARL allows the precise and unique specification of the functionality of a knowledge-based system independent of any implementational details. A KARL model of expertise contains the description of domain knowledge, inference knowledge, and procedural control knowledge. For capturing these different types of knowledge KARL provides corresponding modeling primitives that are based on Frame-logic and Dynamic Logic. A declarative semantics for a complete KARL model of expertise is...
Comparative Metric Semantics for Commit in Or-Parallel Logic Programming
- Eneia Todoran; Jerry den Hartog; Erik de Vink
For the control flow kernel of or-parallel Prolog with commit an operational and a denotational model are constructed and related using techniques from metric semantics. By maintaining explicit scope information a compositional handling of the commit for the denotational model is established. By application of an abstraction function, which deletes this extra information, the operational semantics is recovered. 1 Introduction In recent years substantial progress has been reported on or-parallel logic programming systems, on successful experiments with extensive test sets performed on it, as well as on and-parallel extensions of these systems. See, e.g., [11, 13, 5, 10]. However, ...
Unnatural Language Discourse: An Empirical Study of Multimodal Proof Styles
- Jon Oberlander; Padraic Monaghan; Richard Cox; Keith Stenning; Richard Tobin
Computer-based logic proofs are a form of `unnatural' language discourse, but the structure and process of proof generation can be observed in considerable detail, and analysis is leading to a number of general insights. We have been studying how students respond to multimodal logic teaching. Performance measures have already indicated that students' pre-existing cognitive styles have a significant impact on teaching outcome. Furthermore, a large corpus of proofs has been gathered via automatic logging of proof development. This paper applies a series of techniques, including corpus statistical methods, to the proof logs. The results indicate that students' cognitive styles influence...
Logic Synthesis Based on the Reed-Muller Representation
- Jonathan Saul
There has been recent interest in using Reed-Muller equations as a way of representing and manipulating switching functions, and as a means of designing circuits based on exclusiveOR gates. Analysis of existing algorithms suggests the need for work in three areas: improving two-level minimization algorithms; developing algorithms for multi-level minimization; and then using the new algorithms to verify the usefulness of Reed-Muller equations in practical applications. A new algorithm for the two-level minimization of Reed-Muller representations of switching functions has been developed, in which new heuristics are used to determine the best application of previously known rules for minimizing single...
Application Of Fuzzy Logic And Neural Network To The Control Of A Flame Process
- Wenjing Tao; Hans Burkhardt
this paper we will discuss our control system un-