On the Intuitionistic Force of Classical Search
- Eike Ritter; David Pym; Lincoln Wallen
The combinatorics of classical propositional logic lies at the heart of both local and global methods of proof search due to the possibility to achieve least-commitment search. Extension of such methods to the predicate calculus, or to non-classical systems, presents us with the problem of recovering this least-commitment principle in the context of non-invertible rules. One successful approach is to view the nonclassical logic as a perturbation on search in classical logic and characterize when a least-commitment (classical) search yields sufficient evidence for provability in the (non-classical) logic. This technique has been successfully applied to both local and global methods...
Verification via Tableaux
- Marian Srebrny; Instytut Podstaw Informatyki; Polskiej Akademii Nauk
We present a set of seminar notes on basic concepts and results on automated and semiautomated verification of correctness and validation of software systems (protocols) via the method of tableaux, often called semantic tableaux. Special emphasis is on comparison of various ways of formalization of the concept of a `proof ', on the example of the classical first-order logic. 1 Introduction Gentzen  proposed two distinct formalizations of deduction systems. Each of them in both classical and intuitionistic versions. Only one of them he called natural deduction. The second he called the logistic calculus. In this presentation we distinguish the...
Some Notes on Logic Programming with a Relational Machine (Extended Abstract)
- James Lipton; Emily Chapman
) James Lipton Emily Chapman Dept. of Mathematics, Wesleyan University Abstract We study the use of relation calculi for compilation and execution of Horn Clause programs with an extended notion of input and output. We consider various other extensions to the Prolog core. 1 Introduction Logic programming is programming with predicates in a certain fragment of logic. More broadly speaking, it is programming with executable specifications: code that has independent mathematical meaning consistent with its input-output behavior. Specifications are often formalized as relations. In this paper we explore how Logic Programming itself may be profitably understood, extended and compiled in...
The Complexity of Concept Languages
- F. M. Donini; M. Lenzerini; D. Nardi; W. Nutt
The basic feature of Terminological Knowledge Representation Systems is to represent knowledge by means of taxonomies, here called terminologies, and to provide a specialized reasoning engine to do inferences on these structures. The taxonomy is built through a representation language called concept language (or description logic), which is given well-defined set-theoretic semantics. The efficiency of reasoning has often been advocated as a primary motivation for the use of such systems. Deduction methods and computational properties of reasoning problems in concept languages are the subject of this paper. The main contributions of the paper are: (1) a complexity analysis of concept...
Temporal Triggers in Active Databases
- Prasad Sistla; Ouri Wolfson
In this paper we propose two languages, called Future Temporal Logic (FTL) and Past Temporal Logic (PTL), for specifying temporal triggers. Some examples of trigger conditions that can be specified in our language are the following: "The value of a certain attribute increases by more than 10% in ten minutes", "A tuple that satisfies a certain predicate is added to the database at least 10 minutes before another tuple, satisfying a different condition, is added to the database". Such triggers are important for monitor and control applications. In addition to the languages, we present algorithms for processing the trigger conditions...
Concurrent Actions and Changes in the Situation Calculus
- José Júlio Alferes; Renwei Li; Alferes Renwei; Luís Moniz Pereira
In this paper we investigate concurrent actions and changes. We extend the standard situation calculus with concurrent actions and show that the extended situation calculus has the same expressive power as the original one. In the extended situation calculus we identify and focus on the composition problem which relates effects of concurrent actions to those of their component actions. A defeasible solution to the composition problem is proposed. The believability of some choices of default rules for the composition problem and atomicity of actions are discussed. We also provide some simple examples to illustrate the usefulness of our defeat rules....
Specification of Dynamics for Knowledge-based Systems
- Pascal Van Eck; Joeri Engelfriet; Dieter Fensel; Frank Van Harmelen; Yde Venema; Mark Willems
. During the last years, a number of formal specification languages for knowledge-based systems have been developed. Characteristic for knowledge-based systems are a complex knowledge base and an inference engine which uses this knowledge to solve a given problem. Specification languages for knowledge-based systems have to cover both aspects: they have to provide means to specify a complex and large amount of knowledge and they have to provide means to specify the dynamic reasoning behaviour of a knowledge-based system. This paper will focus on the second aspect, which is an issue considered to be unsolved. For this purpose, we have...
Modelling Agent Interaction in Logic Programming
- Luís Moniz Pereira; Lu'is Moniz Pereira; Paulo Quaresma; Centria Ai Centre
We present a logic programming framework implemented over Prolog which is able to model an agent's mental state. An agent is modeled by a set of extended logic programming rules representing the agent's behavior, attitudes (beliefs, intentions, and goals), world knowledge, and temporal and reasoning procedures. At each stage the agents's mental state is defined by the well founded model of the extended logic program plus some constraints. Via this modeling an agent is able to interact with other agents, updating and revising its mental state after each event. The revision process includes the ability to remove contradictions in the...
Distance: a New Metric for Controlling Granularity for Parallel Execution
- Kish Shen; Vítor Santos Costa; Andy King
Granularity control is a method to improve parallel execution performance by limiting excessive parallelism. The general idea is that if the gain obtained by executing a task in parallel is less than the overheads required to support parallel execution, then the task is better executed sequentially. Traditionally, in logic programming task size is estimated from the sequential time-complexity of evaluating the task. Tasks are only executed in parallel if task size exceeds a pre-determined threshold. We argue in this paper that the estimation of complexity on its own is not an ideal metric for improving the performance of parallel programs...
A Modal µ-Calculus and a Proof System for Value Passing Processes
- D.B. Gurov; S. Berezin; B.M. Kapron
A first-order modal ¯-calculus is introduced as a convenient logic for reasoning about processes with value passing. For this logic we present a proof system for model checking sequential processes defined in the value passing CCS. Soundness of the proof system is established. The use of the system is demonstrated on two small but instructive examples. 1 Introduction The propositional modal ¯-calculus is a particularly expressive logic for reasoning about branching-time properties of communicating systems. Many other logics, like dynamic logic and CTL, have uniform encodings in this logic . Over the last decade, many proof systems for checking validity...
Towards a Closer Integration of Finite Domain Propagation and Simplex-Based Algorithms
- T. Hajian; H. El-sakkout; M. Wallace; J. M. Lever; E.B. Richards
This paper describes our experience in implementing an industrial application using the Finite Domain solver of the ECL i PS e Constraint Logic Programming (CLP) system, in conjunction with the Mathematical Programming (MP) system, FortMP. In this technique, the ECL i PS e system generates a feasible solution that is adapted to construct a starting point (Basic solution) for the MP solver. The Basic solution is then used as an input to the FortMP system to warm-start the Simplex (SX) algorithm, hastening the solution of the linear programming relaxation, (LPR). SX proceeds as normal to find the optimal integer solution....
Using Tabled Logic Programming and Preference Logic for Data Standardization
- Baoqiu Cui; Terrance Swift; David S. Warren
We define standardization as the process of extracting useful information from poorly structured textual data. This process includes correcting misspellings and truncations, extraction of data via parsing, and correcting inconsistencies in extracted data. Prolog programming offers natural advantages for standardizing: definite clause grammars can be used to parse data; Prolog rules can be used to correct inconsistencies; and Prolog's simple syntax allows rules to be generated to correct misspellings and truncations of keywords. At least one commercial standarizer has exploited these advantages, but recent advances in tabling and in non-monotonic reasoning have allowed even more powerful and declarative standardizers to...
Compositional Semantics for Unification-based Linguistic Formalisms
- Shuly Wintner
Contemporary linguistic formalisms have become so rigorous that it is now possible to view them as very high level declarative programming languages. Consequently, grammars for natural languages can be viewed as programs; this view enables the application of various methods and techniques that were proved useful for programming languages to the study of natural languages. This paper adapts the notion of program composition, well developed in the context of logic programming languages, to the domain of linguistic formalisms. We study alternative definitions for the semantics of such formalisms, suggesting a denotational semantics that we show to be compositional and fully-abstract....
Logic Programming with Bunched Implications (Extended Abstract)
- David J. Pym
) David J. Pym Department of Computer Science, Queen Mary and Westfield College, University of London Abstract We introduce the logic of bunched implications, BI, in which multiplicative (or linear) and additive (or intuitionistic) implications live side-by-side. We provide a truth conditional semantics, a proof theory and a categorical semantics of proofs. We explain how BI arises as a logic of resources and sketch a development of this computational interpretation, which is quite different from that of linear logic, in the setting of logic programming. Predicate BI, used in our account of logic programming, admits not only the usual (additive)...
Activity-Monitoring Completion-Detection (AMCD): A new single rail approach to achieve self-timing
- Grass Morling; E. Grass; R. C. S. Morling; I. Kale
A new method for designing single rail asynchronous circuits is studied. It utilises additional circuitry to monitor the activity of nodes within combinational logic blocks. When all transitions have halted a completion signal is generated. Details of the circuit and design methodology are given and the influence of glitches on the proposed circuit is discussed. Three different levels of granularity are investigated. Experimental physical layout of the circuit with extracted and back-annotated simulation results is provided. The proposed approach results in faster operation than synchronous circuits with minimum circuit overhead incurred. 1 Introduction The difficulty in distributing a high speed...
Learning Simple Phonotactics
- Erik F. Tjong; Kim Sang; John Nerbonne
The present paper compares stochastic learning (Hidden Markov Models) , symbolic learning (Inductive Logic Programming), and connectionist learning (Simple Recurrent Networks using backpropagation) on a single, linguistically fairly simple task, that of learning enough phonotactics to distinguish words from non-words for a simplified set of Dutch, the monosyllables. The methods are all tested using 10% reserved data as well as a comparable number of randomly generated strings. Orthographic and phonetic representations are compared. The results indicate that while stochastic and symbolic methods have little difficulty with the task, connectionist methods do. 1 Introduction This paper describes a study of the...
The Logical Impingement of AI
- Luís Moniz Pereira; Lu#s Moniz Pereira
We address the impingement of AI on logic, by examining the requirements posed on logic by knowledge representation and reasoning issues which AI has addressed. We then outline some of AI's contributions, via Logic Programming, to more dynamic forms of logic, in order to deal with knowledge in flux, namely: incomplete and contradictory information; hypotheses making through abduction; argumentation; diagnosis and debugging; updating; and learning. Along the way we delve into implications for the philosophy of knowledge. Our motivation is to entice the philosophically inclined readership to the new territories recently landmarked in the logical continent by ongoing research in...
What's in an Aggregate: Foundations for Description Logics with Tuples and Sets
- Giuseppe De Giacomo; Maurizio Lenzerini
Based on the research done in the last decade, attempts have been made to propose description logics as unifying formalisms for the various class-based representation languages used in different areas. These attempts have made apparent that sound, complete, and decidable description logics still suffer from several limitations, regarding modeling classes of aggregate objects, expressing general inclusion axioms, and the ability of navigating links between classes. In this paper we make description logics accomplish the necessary leap in order to become suitable for the new challenging applications they are faced with. In particular, we propose a powerful description logic overcoming the...
Declarative Continuations and Categorical Duality
- Andrzej Filinski
This thesis presents a formalism for reasoning about continuations in a categorical setting. It points out how values and continuations ca n be seen as categorically dual concepts, and that this symmetry extends to not only data types, but also control structures, evaluation strategies and higher-order constructs. The central idea is a view of continuations as a declarative concept, rather than an imperative one, and the implicat ions of this make up the spine of the presentation. A symmetrical extension of the typed *-calculus is introduced, where values and continuations are treated as opposites, permitting a mirror-image syntax for dual...
Context-Dependent Reasoning With Lexical Knowledge Using Default Logic
- Anthony Hunter
Lexical knowledge is increasingly important in language engineering. However, it is a difficult kind of knowledge to represent and reason with. Existing approaches to formalizing lexical knowledge have used languages with limited expressibility and in particular they have not addressed the context-dependent nature of lexical knowledge. Here we present a framework, based on default logic, called the dex framework, for capturing context-dependent reasoning with lexical knowledge. Default logic is a first-order logic offering a more expressive formalisation than inheritance hierarchies: (1) First-order formulae about words can be inferred; (2) Preferences over formulae can be based on specificity, reasoning about exceptions,...