221.
Implementation of Threshold Logic
- Alexander Stokman
Traditionally, logic circuits have been, and are still being implemented using Boolean logic. Although there has been a tremendous increase in the performance of the technology used to implement Boolean logic primitives, the underlying paradigm has remained unchanged over the years. Since the early 1960's there is a fundamentally more powerful alternative for Boolean logic available, called Threshold Logic (TL). Although implementations of TL gates have grown with the advances in technology, none of these have ever proven widely applicable. Because of this TL was never a practical success. Recently a new technology called Capacitive Threshold Logic (CTL) was disclosed...
222.
Computational Logic
- Maria H. Napierala
COMPUTATIONAL LOGIC
Maria H. Napierala, Ph.D.
Oregon Graduate Institute 1992
Supervising Professor: Richard B. Kieburtz
This thesis resulted from the research on relating classical and constructive proofs. It is well
known that constructive type theories constitute formal systems for constructive mathematics.
In these theories the constructivity is implicit in the restriction to intuitionistic logic. This
means that restrictions are placed both on the objects studied and on the methods of proofs
which may be applied. Hence, not all logical laws (e.g., law of excluded middle, proof by
contradiction) can be used in the proofs of consistency of logical specifications. Thus,
constructive type theories are reasoning systems only for purely functional...
223.
To appear in Theory and Practice of Logic Programming (TPLP) 1 Embedding Defeasible Logic into Logic Programming
- Grigoris Antoniou; David Billington; Guido Governatori; Michael J. Maher
Defeasible reasoning is a simple but efficient approach to nonmonotonic reasoning that has recently attracted considerable interest and that has found various applications. Defeasible logic and its variants are an important family of defeasible reasoning methods. So far no relationship has been established between defeasible logic and mainstream nonmonotonic reasoning approaches. In this paper we establish close links to known semantics of logic programs. In particular, we give a translation of a defeasible theory D into a meta-program P (D). We show that under a condition of decisiveness, the defeasible consequences of D correspond exactly to the sceptical conclusions of...
224.
Linear Logic,
- R. A. G. Seely
A brief outline of the categorical characterisation of Girard's
linear logic is given, analagous to the relationship between cartesian closed categories
and typed -calculus. The linear structure amounts to a -autonomous
category: a closed symmetric monoidal category G with finite products and a
closed involution. Girard's exponential operator, ! , is a cotriple on G which
carries the canonical comonoid structure on A with respect to cartesian product
to a comonoid structure on !A with respect to tensor product. This makes the
Kleisli category for ! cartesian closed.
0.
225.
Programming in Logic
This article
describes the abstract model implicit in logic programming and compares it to
the models used in conventional languages. A simple example in Prolog
illustrates how programming in logic can provide a concise problem description
while offering a very flexible framework to solve for unknowns. The last section
of this article surveys the current fields of active research in the area of logic
programming and concludes with a prognosis for the future of this method
226.
Taming First-Order Logic
- Szabolcs Mikul As
In this paper we define computationally well-behaved versions of classical first-order logic and prove that the validity problem is decidable 1 . Keywords : first-order logic, decidability, relativization, mosaic, polyadic and counting quantifiers. 1Taming In [5], we developed a strategy for taming logics. The idea of taming can be described as follows. Let us assume that we have a well-investigated logic with some undesirable metalogical properties. An example is the incompleteness and undecidability of the finite variable fragment of classical first-order logic, FOL, with at least three variables, cf. [4] 4.1.3 and 4.2.18 for the equivalent algebraic results. Taming a...
227.
Abstract Interpretation of Linear Logic Programming
- Jean-marc Andreoli; Tiziana Castagnetti; Remo Pareschi
Linear Logic is gaining momentum in computer science because it offers a unified framework and a common vocabulary for studying and analyzing different aspects of programming and computation. We focus here on models where computation is identified with proof search in the sequent system of Linear Logic. A proof normalization procedure, called "focusing", has been proposed to make the problem of proof search tractable. Correspondingly, there is a normalization procedure mapping formulae of Linear Logic into a syntactic fragment of that logic, called LinLog, and in which the focusing normalization for proofs can be most conveniently expressed. In this paper,...
228.
Topology via Constructive Logic
By working constructively in the sense of geometric logic, topology can be hidden. This
applies also to toposes as generalized topological spaces.
1
229.
Executing Suspended Logic Programs
- Robert A. Kowalski; Francesca Toni; Gerhard Wetzel
We present an extension of Logic Programming (LP) which, in addition to ordinary LP clauses, also includes integrity constraints, explicit representation of disjunction in the bodies of clauses and in goals, and suspension of atoms as in concurrent logic languages. The resulting framework aims to unify Constraint Logic Programming (CLP), Abductive Logic Programming (ALP) and Semantic Query Optimisation (SQO) in deductive databases. We present a proof procedure for the new framework, simplifying and generalising previously proposed proof procedures for ALP. We discuss applications of the framework, formulating traditional problems from LP, ALP, CLP and SQO.
230.
A KANTIAN LECTURE OF STANDARD DEONTIC LOGIC
- Gisele Dalva Secco
A presente dissertação é o resultado de uma investigação acerca da semântica para lógica deôntica standard. Restringindo-se à versão proposicional da mesma, o trabalho teve como principal objeto de estudo alguns textos do filósofo J. Hintikka, cuja proposta de semântica para lógica deôntica inclui a reinterpretação de uma noção importante da filosofia de I. Kant: a noção de Reino dos Fins. Kant também figura na proposta de Hintikka pela ilustração de um dos resultados de sua abordagem, a saber, a distinção entre conseqüência lógica e conseqüência deôntica, da qual o assim chamado princípio de Kant é um exemplo. Tendo como...
231.
Intelligent Traffic Lights Control By Fuzzy Logic
- Tan Kok Khiang; Marzuki Khalid; Rubiyah Yusof; Universiti Teknologi Malaysia; Jalan Semarak
One of the ways to overcome traffic problems in large cities is through the development of an intelligent monitoring and control of traffic lights system. This paper addresses the design and implementation of an intelligent traffic lights controller based on fuzzy logic technology. A software has been developed to simulate the situation of an isolated traffic junction based on this technology. The software is highly graphical in nature and uses the Windows system. The software allows simulation of different traffic conditions at the junction and comparison can be made between the fuzzy logic controller and a conventional fixed-time controller. Simulation...
232.
Default Logic and Specification of Nonmonotonic Reasoning
- Joeri Engelfriet; V. Wiktor Marek; Jan Treur; Miroslaw Truszczynski
In this paper constructions leading to the formation of belief sets by agents are studied. The focus is on the situation when possible belief sets are built incrementally in stages. An infinite sequence of theories that represents such a process is called a reasoning trace. A set of reasoning traces describing all possible reasoning scenarios for the agent is called a reasoning frame. Default logic by Reiter is not powerful enough to represent reasoning frames. In the paper a generalization of default logic of Reiter is introduced by allowing infinite sets of justifications. This formalism is called infinitary default logic....
233.
Translating a Linear Logic Programming Language into Java
- Mutsunori Banbara; Naoyuki Tamura
There have been several proposals for logic programming language based on linear logic: Lolli [8], Lygon [7], LO [3], LinLog [2], Forum [11], HACL [10]. In these languages, it is possible to create and consume resources dynamically as logical formulas. The e#cient handling of resource formulas is, therefore, an important issue in the implementation of these languages. Lolli, Lygon, and Forum are implemented as interpreter systems; Lolli is on SML and #Prolog, Lygon is on Prolog, Forum is on SML, #Prolog and Prolog. However, none of them have been implemented in Java. In this paper, we describe the Prolog Cafe...
234.
A descriptive Mode Inference for Logic Programs
- Ebénézer Ntienjem; Copyright C Fl Eb'en'ezer Ntienjem
In general, an n-ary predicate (relation) describes the relationship among its arguments, and such that no argument has to be of a special mode. The unification and the resolution (SLDNF-resolution) do capture this state of affair. Hence, the aim of logic programming is in some point approximatively achieved if the system is able to automatically determine the descriptive mode of an n-ary predicate symbol with respect to a logic program. The descriptive mode of an n-ary predicate symbol with respect to a logic program indicates the instantiation of the arguments of that n-ary predicate symbol when it occurs in a...
235.
Composing and Refining Dense Temporal Logic Specifications
- Antonio Cau
. A dense temporal logic development method for the specification, refinement, composition and verification of reactive systems is introduced. A reactive system is specified by a pair consisting of a machine and a condition that indicate the valid computations of this machine. Compositionality is achieved by adding to each machine step whether it is a environment, system or communication step. Refinement can be expressed straightforward in the logic because the stutter problem is elegantly solved by using the dense structure of the logic. Compositionality enables us to break refinement between complex systems into refinement between small and simple systems. The...
236.
A Linear Logic View of Object Systems
- Berndt Farwer
Linear Logic [Gir87] has been shown to incorporate a fragment suitable for representing P/T-nets and giving a semantics to the computations of such nets (e.g. [Bro89], [MOM89], [EW90]). This result is generalized to coloured nets. Furthermore a new kind of Petri nets is dened: Linear Logic Petri Nets (LLPN). These nets are used as an intuitive semantics to well-known and new high level net concepts. keywords: Linear Logic, Petri nets, object systems, concurrency 1 Introduction Petri nets have been used successfully throughout the last three decades for the specication and analysis of a diverse range of problems. The theory of...
237.
Cactus: A Branching-Time Logic Programming Language
- Rondogiannis Gergatsoulis; P. Rondogiannis; M. Gergatsoulis; T. Panayiotopoulos
. Temporal programming languages are recognized as natural and expressive formalisms for describing dynamic systems. However, most such languages are based on linear flow of time, a fact that makes them unsuitable for certain types of applications. In this paper we introduce the new temporal logic programming language Cactus, which is based on a branching notion of time. In Cactus, the truth value of a predicate depends on a hidden time parameter which has a tree-like structure. As a result, Cactus appears to be especially appropriate for expressing non-deterministic computations or generally algorithms that involve the manipulation of tree data...
238.
Cactus: A Branching-Time Logic Programming Language
- P. Rondogiannis; M. Gergatsoulis; T. Panayiotopoulos
. Temporal programming languages are recognized as natural and expressive formalisms for describing dynamic systems. However, most such languages are based on linear flow of time, a fact that makes them unsuitable for certain types of applications. In this paper we introduce the new temporal logic programming language Cactus, which is based on a branching notion of time. In Cactus, the truth value of a predicate depends on a hidden time parameter which has a tree-like structure. As a result, Cactus appears to be especially appropriate for expressing non-deterministic computations or generally algorithms that involve the manipulation of tree data...
239.
A Hybrid Projection Temporal Logic for Hybrid Systems
- Zhenhua Duan; Mike Holcombe
This paper proposes a specification language, Hybrid Projection Temporal Logic (HPTL), for the purpose of modelling, analyzing and verifying hybrid systems consisting of a non-trivial mixture of discrete and continuous components. The syntax and semantics of HPTL are presented, and some examples of hybrid systems are modelled with HPTL to illustrate the formalism. Keywords: Temporal logic, statecharts, X-machine, automaton, hybrid system. 1 Introduction Hybrid systems are systems that consist of a non-trivial mixture of continuous activities and discrete events. To model, analyze, verify, and control such a system, various kinds of formalisms based on finite state machines, e.g. phase transition...
240.
Architectural Specification and Simulation Through Rewriting-Logic
- Mauricio Ayala-Rincon Departamento; Carlos H. Llanos
In recent years Arvind's Group at MIT has shown the usefulness of term rewriting theory for the specification of processor architectures. In their approach processors specified by term rewriting systems are translated into a standard hardware description language for simulation purposes. In this work we present our current investigation on the use of Rewriting-Logic, which is a more powerful theoretical framework than pure rewriting, for specification and verification of processor architectures at a higher abstraction level. We adopt the rewriting-logic environment ELAN to specify and verify architectures without the need to resort to the details of hardware description languages for...
