A Multistrategy Approach to Relational Knowledge Discovery in Databases
- Katharina Morik; Peter Brockhausen
When learning from very large databases, the reduction of complexity is of highest importance. Two extremes of making knowledge discovery in databases (KDD) feasible have been put forward. One extreme is to choose a most simple hypothesis language and so to be capable of very fast learning on real-world databases. The opposite extreme is to select a small data set and be capable of learning very expressive (firstorder logic) hypotheses. A multistrategy approach allows to combine most of the advantages and exclude most of the disadvantages. More simple learning algorithms detect hierarchies that are used in order to structure the...
Extensible Knowledge Base Management for Description Logics
- Alex Borgida
Description Logics form a family of decidable knowledge representation and reasoning languages, which have been applied with increasing success to problems of data and information management, as techniques for meta-data and query description. As all other logical representational formalisms, DLs are subject to the familiar expressivenesstractability tradeoff, which leave users unhappy either because the language is not rich enough to express everything desired, or because the implementation is too slow or incomplete in unpredictable ways. This paper offers a new alternative for approaching this dilemma: a modularized software architecture for DL-based KBMS, which supports both through its structure and through...
Typing First-Class Continuations in ML
- Robert Harper; Bruce F. Duba; David Macqueen
An extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A continuation-based operational semantics is defined for a small, purely functional, language, and the soundness of the Damas-Milner polymorphic type assignment system with respect to this semantics is proved. The full Damas-Milner type system is shown to be unsound in the presence of first-class continuations. Restrictions on polymorphism similar to those introduced in connection with reference types are shown to suffice for soundness. 1 Introduction First-class continuations are a simple and...
The Logic of Provability
- Giorgi Japaridze; Dick De Jongh
Contents 1. Introduction, Solovay's theorems . . . . . . . . . . . . . . . . . . . . . . . . . . 476 2. Modal logic preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 477 3. Proof of Solovay's theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . ....
System Description: Verification of Distributed Erlang Programs
- Thomas Arts; Mads Dam; Lars-åke Fredlund; Lars-ake Fredlund; Dilian Gurov
Introduction Software written for telecommunication applications has to meet high quality demands. Correctness is one major concern; the activity of proving formally that a system is correct is called verification. Telecommunications software is highly concurrent, and testing is often not capable of guaranteeing correctness to a satisfactory degree. The software we are faced with consists of many, relatively small modules, written in the functional language Erlang [AVWW96]. These modules define the behaviour of a number of processes operating in parallel and communicating through asynchronous message-passing. New processes can be generated during execution. Because of the complexity of such software, our...
Theorem Proving and Partial Proof Search for Intuitionistic Propositional Logic Using a Permutation-free Calculus with Loop Checking
- Jacob Howe
this paper the history mechanism is developed in two ways and applied to
A Fine-Grained Model for Code Mobility
- Gruia-catalin Roman; Cecilia Mascolo; Cecilia Mascolo; Gian Pietro Picco; Gian Pietro Picco
. In this paper we take the extreme view that every line of code is potentially mobile, i.e., may be duplicated and/or moved from one program context to another on the same host or across the network. Our motivation is to gain a better understanding of the range of constructs and issues facing the designer of a mobile code system, in a setting that is abstract and unconstrained by compilation and performance considerations traditionally associated with programming language design. Incidental to our study is an evaluation of the expressive power of Mobile Unity, a notation and proof logic for mobile...
Typology and Logical Structure of Natural Languages
- Vincenzo Manca
This paper focuses on some relationships between logic and natural languages, a topic that is crucial in Western philosophy (From Aristotle, to medieval Modistae, to Leibniz and the founders of modern mathematical logic). Specifically, the search for a universal grammar is considered in connection with linguistic typology (see Greenberg 's Universals of Grammar) and formalisms for knowledge representation (see Kamp, Moore). A preliminary investigation proves that usual linguistic concepts could be incorporated into a formal theory of general explicative power. This suggests a logical theory of grammars, where classical linguistic analysis is generalized and formalized. The conceptual and terminological apparatus...
Improving Backward Execution in Non-Deterministic Concurrent Logic Languages
- Salvador Abreu; Luís Moniz Pereira; Philippe Codognet; Lu'is Moniz Pereira
We present a new mechanism for improving the execution of non-deterministic concurrent logic languages, such as the Andorra family of languages. The basic idea is, upon failure and backtracking, to re-schedule continuation goals in order to first execute the goal that has failed. In this way, if the backtrack point is not pertinent to the failure, the original failing goal will fail again and this will immediately amount to further deeper backtracking. Such a heuristic will hence save useless deduction /backtracking work. This method would be very difficult to implement in sequential stack-based logic systems such as Prolog, but fits...
Reasoning about Actions with Abductive Logic Programming
- Luís Moniz Pereira; Renwei Li
In order to construct a computer-based system which can reason and act intelligently in the real world, we have to develop a computational but provably correct methodology and its related software system which can reason about actions and changes in dynamic domain. For this purpose we propose to use abductive logic programming paradigm as the computational mechanism. Technically, we make use of a simple, but extensible if needed, action description language to describe the domain in question. Then we use a sound and complete translation algorithm to transform domain descriptions into abductive logic programs. And thus reasoning about actions is...
GULP 2.0: An Extension of Prolog for Unification-Based Grammar
- Michael A. Covington
ABSTRACT: A simple extension to Prolog facilitates implementation of unification-based grammars (UBGs) by adding a new notational device, the feature structure, whose behavior emulates graph unification. For example, a:b..c:d denotes a feature structure in which a has the value b, c has the value d, and the values of all other features are unspecified. A modified Prolog interpreter translates feature structures into Prolog terms that unify in the desired way. Thus, the extension is purely syntactic, analogous to the automatic translation of "abc" to [97,98,99] in Edinburgh Prolog. The extended language is known as GULP (Graph Unification Logic Programming); it...
A Verification Environment for I/O Automata -- Part II: Theorem Proving and Model Checking
- Olaf Müller
We describe a verification framework for I/O automata in Isabelle. It includes a temporal logic, proof support for showing implementation relations between live I/O automata, and a combination of Isabelle with model checking via a verified abstraction theory. The underlying domain-theoretic sequence model turned out to be especially adequate for these purposes. Furthermore, using a tailored combination of Isabelle's logics HOL and HOLCF we achieve two complementary goals: expressiveness for proving meta theory (HOLCF) and simplicity and efficiency for system verification (HOL).
Logical Foundations of Object-Oriented and Frame-Based Languages
- Michael Kifer; Georg Lausen; James Wu
We propose a novel formalism, called Frame Logic (abbr., F-logic), that accounts in a clean and declarative fashion for most of the structural aspects of object-oriented and frame-based languages. These features include object identity, complex objects, inheritance, polymorphic types, query methods, encapsulation, and others. In a sense, F-logic stands in the same relationship to the objectoriented paradigm as classical predicate calculus stands to relational programming. F-logic has a model-theoretic semantics and a sound and complete resolution-based proof theory. A small number of fundamental concepts that come from object-oriented programming have direct representation in F-logic
A Logic for Conditional Recommendation
- Das William; S. K. Das; P. Hammond
ere malfunction or operator error may give rise to severe injury, death or financial /environmental catastrophe with the potential for legal liability. The work presented here arises from our involvement in a project addressing the technology and legal implications of knowledgebased decision support systems in safety-critical domains. To illustrate and motivate the abstract notions, we give examples in the domain of decision support in oncology, a specific interest of one of the project partners. Because of the complexity of treatment performed and the amount of data captured during oncology trials, computerized decision support is essential. The safety-critical aspect arises from...
IAP for Dummies: The YAP Design
- Manuel Eduardo Correia; Vítor Santos Costa; Manuel Eduardo; Manuel Eduardo; Santos Costa; Santos Costa
One of the advantages of logic programming is the fact that it offers several sources of implicit parallelism. One particularly interesting form of And-Parallelism is Independent And-Parallelism (IAP). Most work on the implementation of IAP is based on Hermenegildo's RAP-WAM. Unfortunately there are some drawbacks associated with the classical approaches based on the use of parcalls and markers. One first observation is that the introduction of parcall frames significantly slows down sequential execution. Moreover, it may result in fine-grained parallel work. We found these problems to be particularly significant in the context of the implementation of combined AND/OR systems. In...
Efficient Distribution by Static Analysis
- André Spiegel
. Distribution is an aspect of parallel programming that becomes increasingly well understood and handled ever more transparently on recently developed distribution platforms. We show in this paper that the performance of such platforms can be improved by static information about a program's logic and structure which is impossible to determine at run-time. Examples for this include object immutability and the dynamic scoping of object references. We present a set of static analysis algorithms that can obtain this information automatically, and we introduce an automatic distribution environment called Pangaea which we are currently building to use these algorithms for parallel,...
Technology Mapping for Lookup-Table Based Field-Programmable Gate Arrays
- Robert J. Francis
Field Programmable Gate Arrays (FPGAs) provide a new approach to Application Specific Integrated Circuit (ASIC) implementation that features both large scale integration and user programmability. The logic capacity of these devices is large enough to make automated synthesis essential for the efficient design of FPGA circuits. This thesis focuses on the class of FPGAs that use lookup tables (LUTs) to implement combinational logic. A K-input lookup table is a digital memory that can implement any Boolean function of K variables. Lookup table circuits present new challenges for logic synthesis, particularly technology mapping, which is the phase of logic synthesis directly...
Verification of Parameterized Systems Using Logic Program Transformations
- Abhik Roychoudhury; K. Narayan Kuamr; C. R. Ramakrishnan; I. V. Ramakrishnan; Scott A. Smolka
We show how the problem of verifying parameterized systems can be reduced to the problem of determining the equivalence of goals in a logic program. We further show how goal equivalences can be established using induction-based proofs. Such proofs rely on a powerful new theory of logic program transformations (encompassing unfold, fold and goal replacement over multiple recursive clauses), can be highly automated, and are applicable to a variety of network topologies, including uni- and bi-directional chains, rings, and trees of processes. Unfold transformations in our system correspond to algorithmic model-checking steps, fold and goal replacement correspond to deductive steps,...
Logic in the Finite
- Scott Weinstein
this paper was completed. I am especially grateful to Steven Lindell for a decade of valuable discussions on the topics of this paper and to Mary-Angela Papalaskari for valuable comments on earlier drafts of this paper.
Modeling Planning Domains Systematically
- Susanne Biundo; Werner Stephan
We present a systematic approach to the modular and incremental construction of provably consistent domain models for planning. It is based on a temporal logic framework that in particular allows for the introduction of abstract datatypes which can usefully be applied to mirror the computational aspects of planning problems and their solutions. A formal concept is developed that enables the construction as well as the modification of already existing domain models in a sound manner. This includes well-defined operations for the union, extension, and refinement of domain models.