Dynamic Logic Programming
- J. J. Alferes; J. A. Leite; L. M. Pereira; H. Przymusinska; T. C. Przymusinski
In this paper we investigate updates of knowledge bases represented by logic programs. In order to represent negative information, we use generalized logic programs which allow default negation not only in their bodies but also in their heads.We start by introducing the notion of an update P \Phi U of a logic program P by another logic program U . Subsequently, we provide a precise semantic characterization of P \Phi U , and study some basic properties of program updates. In particular, we show that our update programs generalize the notion of interpretation update. We then extend this notion to...
Logic Programming and Model Checking
- Baoqiu Cui; Yifei Dong; Xiaoqun Du; K. Narayan Kumar; C. R. Ramakrishnan; I. V. Ramakrishnan; Abhik Roychoudhury; Scott A. Smolka; David S. Warren
. We report on the current status of the LMC project, which seeks to deploy the latest developments in logic-programming technology to advance the state of the art of system specification and verification. In particular, the XMC model checker for value-passing CCS and the modal mu-calculus is discussed, as well as the XSB tabled logic programming system, on which XMC is based. Additionally, several ongoing efforts aimed at extending the LMC approach beyond traditional finite-state model checking are considered, including compositional model checking, the use of explicit induction techniques to model check parameterized systems, and the model checking of real-time...
A SAT-based decision procedure for ALC
- Fausto Giunchiglia; Roberto Sebastiani; Franz Baader
The goal of this paper is to describe and thoroughly test a decision procedure, called Ksat, checking satisfiability in the terminological logic ALC. Ksat is said to be SAT-based as it is defined in terms of a decision procedure for propositional satisfiability (SAT). The tests are performed comparing Ksat with, among other procedures, Kris, a state-of-the-art tableau-based implementation of a decision procedure for ALC. Ksat outperforms Kris of orders of magnitude. Furthermore, the empirical results highlight an intrinsic weakeness that tableau-based decision procedures have with respect to SAT-based decision procedures. Franz Baader, Marco Cadoli, Enrico Franconi, Enrico Giunchiglia, Fabio Massacci...
A Metagrammatical Logical Formalism
- Vincenzo Manca
This paper presents a logical formalism for fundamental concepts of traditional grammar. In its basic sense a grammar is simply a system of (informal) rules which try to discriminate correct linguistic expressions from ones that are incorrect, according to an ideal speaker of the language considered. The term traditional grammar refers to the concepts, methods, and terminology, elaborated over the centuries by grammarians, philosophers and linguists, that constitute (more and less consciously) the average linguistic culture: proposition, predicate, substantive, subject, attribute, complement, modifier, determiner, coordination, subordination, anaphora, ellipsis, deixis, and sentence. These concepts are generally used on the basis of...
Characterizations of Classes of Programs by Three-Valued Operators
- Pascal Hitzler; Anthony Karel Seda
. Several important classes of normal logic programs, including the classes of acyclic, acceptable, and locally hierarchical programs, have the property that every program in the class has a unique twovalued supported model. In this paper, we call such classes unique supported model classes. We analyse and characterize these classes by means of operators on three-valued logics. Our studies will motivate the definition of a larger unique supported model class which we call the class of \Phi -accessible programs. Finally, we show that the class of \Phi -accessible programs is computationally adequate in that every partial recursive function can be...
Mechanisms for Combining Logics
- Carlos Caleiro; Cristina Sernadas; Amílcar Sernadas
We consider three paradigmatic combination mechanisms for propositional based logics: synchronization, fibring and parameterization. We introduce our working universes of logic systems and recall their original characterizations, both model and proof-theoretically. We present a novel notion of algebraic logic system presentation where, besides the usual global of entailment, also local entailment is definable over the internal structure endowed to the meaning algebras. We lift the definition of the three mechanisms to the algebraic level. We then study the relationships between the mechanisms: fibring and parameterization are both obtainable directly from synchronization, while synchronization can be seen as a particular case...
Proof-search in Type-theoretic Languages: An Introduction
- D. Galmiche; David J. Pym
We introduce the main concepts and problems in the theory of proof-search in type-theoretic languages and survey some specific, connected topics. We do not claim to cover all of the theoretical and implementation issues in the study of proof-search in type-theoretic languages; rather, we present some key ideas and problems, starting from well-motivated points of departure such as a definition of a type-theoretic language or the relationship between languages and proof-objects. The strong connections between different proof-search methods in logics, type theories and logical frameworks, together with their impact on programming and implementation issues, are central in this context. Keywords:...
Top-Down Query Evaluation for Well-Founded Semantics With Explicit Negation
- José Júlio Alferes; Carlos Viegas Damásio; Luís Moniz Pereira; Alferes Carlos; Lu'is Moniz Pereira
. In this paper we define a sound and complete top-- down semantic tree characterization, that includes pruning rules, of the well--founded semantics for programs extended with explicit negation (WFSX), and compare it to other related approaches. It is amenable to a simple implementation, and by its nature readily allows pre-processing into Prolog, showing promise as an efficient basis for further development. 1 Introduction For some time now, programming in logic has been shown to be a viable proposition. Although Horn clause programming augmented with the NOT operator (i.e. Prolog) under the SLDNF derivation procedure does allow negative conclusions, these...
SIMD Processor Arrays for Image and Video Processing: A Review
- Thinh M. Le; W. M. Snelgrove; S. Panchanathan
SIMD processor arrays are becoming popular for their fast parallel executions of low- to medium-complexity image and video processing algorithms, and most stages of the compression standards (JPEG, H.263, and MPEG's). In many existing techniques, visual data processing algorithms and compression standards possess a high degree of parallelism. In particular, the processing of a certain pixel/block does not generally require data from a distant pixel/block, and the instructions for processing these pixels/blocks are usually identical. Thus, these algorithms map naturally onto the architecture of the SIMD processor arrays. In this paper, the architectures of the recently SIMD processor arrays will...
Tabulation-based Induction Proofs with Application to Automated Verification
- Abhik Roychoudhury; C. R. Ramakrishnan; I.V. Ramakrishnan; S. A. Smolka
XSB  is a tabled logic programming system designed to address shortcomings in Prolog's SLD evaluation mechanism for Horn programs. SLD's poor termination and complexity properties have rendered Prolog unsuitable for deductive database (DDB) and non-monotonic reasoning (NMR) applications. In contrast, XSB's implementation achieves a computationally tight integration of the logic programming (LP), DDB, and NMR paradigms. When tabled resolution is used in XSB (by declaring particular predicates to be tabled), the system automatically maintains a table of predicate invocations and answers, using the table for all equivalent invocations after the first one. Many programs that would loop infinitely in...
Permutability of Proofs in Intuitionistic Sequent Calculi.
- Roy Dyckhoff; Luis Pinto
. We prove a folklore theorem, that two derivations in a cut-free sequent calculus for intuitionistic propositional logic (based on Kleene's G3) are inter-permutable (using a set of basic "permutation reduction rules" derived from Kleene's work in 1952) iff they determine the same natural deduction. The basic rules form a confluent and weakly normalising rewriting system. 1. Introduction There is a folklore theorem that two proofs are "really the same" iff they are interpermutable, using permutations as described by Kleene in [.17.]. For example, [.12.] gives two proofs which "give the same deduction" and "differ only in the order of...
An Adequate First Order Interval Logic
- Zhou Chaochen; Michael R. Hansen
The paper uses left and right neighbourhoods as primitive interval modalities to define other unary and binary modalities of intervals in a first order logic with interval length. A complete first order logic for the neighbourhood modalities is presented. The paper demonstrates how the logic can support formal specification and verification of liveness and fairness, and also of various notions of real analysis. 1 Introduction Interval temporal logics, based on ITL , have shown to be useful for the specification and verification of safety properties of real-time systems. In these logics one can succinctly express properties like: "for all intervals...
Run-time Mapping of Graph-Problem Instances onto Reconfigurable Hardware
- Andreas Dandalis; Andreas D; Viktor Prasanna; Jean-luc Gaudiot
this paper we demonstrated a case-study solution that achieves 6 orders of magnitude speedup over the stateof -the art for mapping graph-problem instances onto FPGAs. The novelty of our approach is that the mapping process performs an incremental adaptation of problemspecific configurations to the input problem instance instead of a complete redesign. Not only does the approach significantly speedup run-time mapping but also produces fast, compact logic which reduces the execution time on hardware as well. Our approach can also be applied to other application domains (e.g., image and signal processing, cryptography) where adaptivity to problem instance is required. We...
A Fixpoint Approach to Second-Order Quantifier Elimination with Applications to Correspondence Theory
- Andreas Nonnengart; Andrzej Szałas
This paper is about automated techniques for (modal logic) correspondence theory. The theory we deal with concerns the problem of finding fixpoint characterizations of modal axiom schemata. Given a modal schema and a semantics based method of translating modal formulae into classical ones, we try to derive automatically a fixpoint formula characterizing precisely the class of frames validating this schema. The technique we consider can, in many cases, be easily applied without any computer support. Although we mainly concentrate on Kripke semantics, our fixpoint approach is much more general, as it is based on the elimination of second-order quantifiers from...
Fast, Sound and Precise Narrowing of the Exponential Function
- Timothy Hickey; Qun Ju
In this paper we present an algorithm for narrowing the constraint y = e x . The algorithm has been designed to be fast by using only IEEE multiplication. The main difficulty is to design algorithms which soundly, rapidly, and precisely compute upper and lower bounds on e x and ln(y). We prove that our algorithms are correct and produce upper and lower bounds which differ by at most 2 ULP. Experiments indicate that the bounds differ by 1 ULP 99.8% of the time. The method we describe is table-driven as is Gal's accurate tables method, but the table is...
Power Semigroups and Polynomial Closure
- Benjamin Steinberg; Faculdade De Ci^encias
We show that if H is a pseudovariety of groups closed under semidirect product with the pseudovariety of p-groups for some prime p, then the pseudovariety of semigroups associated to the Boolean polynomial closure of the LH-languages is P(LH) (the pseudovariety generated by power semigroups of semigroups in LH). The polynomial closure of the LH-languages is similarly characterized. 1 Introduction A common approach to studying rational languages is to attempt to decompose them into simpler parts. Concatenation hierarchies allow this to be done in a natural way which, in addition, has applications to logic and circuit theory . A concatenation...
Agents Learning in a Three-Valued Logical Setting
- Evelina Lamma; Fabrizio Riguzzi; Luís Moniz Pereira
We show that the adoption of a three-valued setting for inductive concept learning is particularly useful for learning in single and multiple agent systems. Distinguishing between what is true, what is false and what is unknown can be useful in situations where decisions have to be taken on the basis of scarce information. Such situation occurs, for example, when an agent incrementally gathers information from the surrounding world and has to select its own actions on the basis of such acquired knowledge. In a three-valued setting, we learn a definition for both the target concept and its opposite, considering positive...
Implementing Disequality in the Lazy Functional Logic Language Babel
- Herbert Kuchen; Francisco Javier López-Fraguas; Juan José Moreno-Navarro; Mario Rodríguez-Artalejo
In this paper, we investigate an implementation of a lazy functional logic language (in particular the language BABEL [MR88,MR92]) which uses disequality constraints for solving equations and building answers. We specify a new operational semantics which combines lazy narrowing with disequality constraints and we define an abstract machine tailored to the execution of BABEL programs according to this semantics. The machine is designed as a quite natural extension of a lazy graph narrowing machine [MKLR90]. Disjunctions of disequalities are handled using the backtracking mechanism.
Hypothetical Reasoning: an application to Optical Music Recognition
- Miguel Ferrand; João Alexandre Leite; Amilcar Cardoso
In this paper we propose a hybrid system that bridges the gap between traditional image processing methods, used for low-level object recognition, and abductive constraint logic programming used for high-level musical interpretation. Optical Music Recognition (OMR) is the automatic recognition of a scanned page of printed music. All such systems are evaluated by their rate of successful recognition; therefore a reliable OMR program should be able to detect and eventually correct its own recognition errors. Since we are interested in dealing with polyphonic music, some additional complexity is introduced as several concurrent voices and simultaneous musical events may occur. In...
Logic Programming Methods for Searching the Web
- Helmut Prendinger
In this paper, we propose a method for approximate reasoning within an abductive logic programming setting. Our investigation is motivated by applying abductive reasoning to the problem of searching the web. Retrieval of user-relevant information is modeled as the task of generating abductive solutions (explanations) to a search query. In order to rule out (logically relevant) solutions (web sites) if they are uninteresting to the user, factual relevance criteria are applied. The main contribution of our paper is a well-founded method of restricting the set of abductive solutions in a way that user-relevant information (i) can be retrieved even if...