Generalization of Clauses under Implication
- Peter Idestam-Almquist
In the area of inductive learning, generalization is a main operation, and the usual definition of induction is based on logical implication. Recently there has been a rising interest in clausal representation of knowledge in machine learning. Almost all inductive learning systems that perform generalization of clauses use the relation `-subsumption instead of implication. The main reason is that there is a well-known and simple technique to compute least general generalizations under `-subsumption, but not under implication. However generalization under `-subsumption is inappropriate for learning recursive clauses, which is a crucial problem since recursion is the basic program structure of...
Constraint Inductive Logic Programming and Its Application to Knowledge Discovery in Databases
- Chunnian Liu; Ning Zhong; Setsuo Ohsuga
this paper, hence not very relevant to KDD. We think that the idea of CILP can be applied to the standard Empirical ILP problem and various ILP techniques: Least General Generalization Relative to Background Knowledge (rlgg) , Inverse Resolution , Top-Down Specialization , etc. Let us look at the Inverse Resolution technique as a case study. This method consists of backward proof steps. An ordinary resolution step takes two clauses C 1 and C 2 and resolves them to produce the resolvent C: Then an inverse resolution step takes C (could be a positive example) and C 1 (could be...
Enhancing Design-for-Test for Active Analog Filters by Using CLP(R)
- Franc Novak; Anton Biasizzo; Igor Mozetic; Marina Santo-Zarnik
We describe a computer-aided approach to automatic fault isolation in active analog filters which enhances the design-for-test (DFT) methodology proposed by Soma (1990). His primary concern was in increased controllability and observability while the fault isolation procedure was sketched only in general terms. We operationalize and extend the DFT methodology by using CLP(R) to model analog circuits and by a model-based diagnosis approach to implement a diagnostic algorithm. CLP(R) is a logic programming language which combines symbolic and numeric computation. The diagnostic algorithm uses different DFT test modes and results of voltage measurements for different frequencies and computes a set...
Coordination in the ImpUnity Framework
- H.J.M. Goeman; J.N. Kok; K. Sere; R. T. Udink
Our main interest in this paper is to investigate how we can combine different systems and languages via a shared tuple space. The languages themselves can be for example standard imperative languages. Hence we study a framework, in which we can have both the possibility for communication via a shared tuple space, and more standard imperative programming constructs. The ImpUNITY framework is an extension of the UNITY framework. It contains several program structuring mechanisms and puts special emphasis on compositional refinement of both specifications and programs. It has an associated temporal logic, formal refinement notions, and program transformation rules. In...
Oracles and Quantifiers
- J.A. Makowsky; Y.B. Pnueli
. We describe a general way of building logics with Lindstrom quantifiers, which capture regular complexity classes on ordered structures with polysize reductions. We then extend this method so as to accommodate complexity classes based on oracle Turing machines. Our main result shows an equivalence between enhancing a logic with a Lindstr om quantifier and enhancing a complexity class with an oracle such that, if K is a set of structures, QK the associated Lindstrom quantifier and L a logic that captures a complexity class D, then the enhanced logic L[K] captures D K - the complexity class of machines...
Mixed Fixpoint Theory for Disjunctive Deductive Databases
- Dietmar Seipel; Ulrich Güntzer; Model Generation T
This paper deals with state generation and model generation for minimal model reasoning. We review the fixpoint theory of two immediate consequence operators for databases, cf. also [LoMiRa 92] and [Fe 93], and prove some useful connections between them. For positive-disjunctive databases D, the first operator T s D is based on hyperresolution. It operates on disjunctice Herbrand states and its least fixpoint is equivalent to the minimal model state MSD of the database, i.e. the set of logical consequences. The second operator T i D operates on sets of Herbrand interpretations and its least fixpoint is the set MMD...
Fundamentals of Model Theory
- William Weiss; Cherie D'Mello
Introduction Model Theory is the part of mathematics which shows how to apply logic to the study of structures in pure mathematics. On the one hand it is the ultimate abstraction; on the other, it has immediate applications to every-day mathematics. The fundamental tenet of Model Theory is that mathematical truth, like all truth, is relative. A statement may be true or false, depending on how and where it is interpreted. This isn't necessarily due to mathematics itself, but is a consequence of the language that we use to express mathematical ideas. What at first seems like a deficiency in...
Undefinedness in Z: Issues for Specification and Proof
- R.D. Arthan; Lovelace Road
. This paper considers the treatment of undefined terms in the Z specification language. We argue, on pragmatic grounds, that specification and proof are activities which place conflicting requirements on the handling of undefinedness. We believe that the conflict can be reconciled by encouraging specifications that are independent of the treatment of undefined terms and by gaining a better understanding of the metatheory of undefinedness. 1 Introduction Mathematical specification languages such as the Z notation  are becoming more widely used in the development of critical systems. A particular advantage of Z is (or should be) its familiar mathematical foundations....
A Logic for Miranda, Revisited
- Simon Thompson
. This paper expands upon work begun in the author's [Tho89], in building a logic for the Miranda functional programming language. After summarising the work in that paper, a translation of Miranda definitions into logical formulas is presented, and illustrated by means of examples. This work expands upon [Tho89] in giving a complete treatment of sequences of equations, and by examining how to translate the local definitions introduced by where clauses. The status of the logic is then examined, and it is argued that the logic extends a natural operational semantics of Miranda, given by the translations of definitions into...
Simplification - A general constraint propagation technique for propositional and modal tableaux
- Fabio Massacci
. Tableau and sequent calculi are the basis for most popular interactive theorem provers for formal verification. Yet, when it comes to automatic proof search, tableaux are often slower than Davis-Putnam, SAT procedures or other techniques. This is partly due to the absence of a bivalence principle (viz. the cut-rule) but there is another source of inefficiency: the lack of constraint propagation mechanisms. This paper proposes an innovation in this direction: the rule of simplification, which plays for tableaux the role of subsumption for resolution and of unit for the Davis-Putnam procedure. The simplicity and generality of simplification make possible...
Many-valued Logic in HOL
- Indra Polak
Many-valued logic is formalized in the logic of the theorem prover HOL [GM93]. We follow an algebraic approach, starting from a Heyting algebra. Using this approach and some useful HOL machinery, we implemented a tautology-checker for a three-valued propositional logic. 1 Introduction Currently, a new specification language is under construction at the department of Computing Science in Groningen, called Almost Formal Specification Language, AFSL [Saa]. The semantics of AFSL is based on a three-valued logic. 1 We want to provide users of AFSL with a proper 'specification environment', analogous to a 'programming environment'. Since logic plays an important role in...
A Comparison of Data Prefetching on an Access Decoupled and Superscalar Machine
- G. P. Jones; Jones Topham
In this paper we investigate the behavior of data prefetching on an access decoupled machine and a superscalar machine. We assess if there are benefits to using the decoupling paradigm given that an out-oforder (o-o-o) superscalar architecture could in principle prefetch to the same degree as an access decoupled machine. We have found that for large issue width the access decoupled machine can hide memory latency more effectively than a single instruction window o-o-o superscalar architecture. Our findings also demonstrate that an access decoupled machine offers the benefit of reducing the complexity of window issue logic. 1 Introduction The future...
A Proof Search System for a Modal Substructural Logic Based on Labelled Deductive Systems
- Hiu Fai Chau
This paper describes a proof search system for a non--classical logic (modal concatenation (substructural) logic) based on Gabbay's Labelled Deductive System (LDS). The logic concerned is treated as a case study. It has some unusual features which combine resource (linear, Lambek Calculus or relevance logics) with modality (intensional, temporal, or epistemic logics), and may have some useful applications in AI and natural language processing. We present axiomatic and LDS style proof theories (two-dimensional label structure) and semantics for the logic. Soundness and completeness results are proved. We show that, for non--classical logic theorem proving, LDS is more flexible than the...
A Partial Instantiation based First Order Theorem Prover
- Vijay Chandru; John Hooker; Anjul Shrivastava; Gabriela Rago
Satisfiability algorithms for propositional logic have improved enormously in recent years. This increases the attractiveness of satisfiability methods for first order logic that reduce the problem to a series of ground-level satisfiability problems. Partial Instantiation for first order satisfiability differs radically from standard resolution based methods. Two approaches to partial instantiation based first order theorem provers have been studied by R. Jeroslow  and by Plaisted and Zhu . Hooker and Rago [8, 9] have described improvements of Jeroslow's approach by a) extending it to logic with functions, b) accelerating it through use of satisfiers, as introduced by Gallo and...
Specialising Logic Programs with respect to Call/Post Specifications
- Annalisa Rossi; Sabina Rossi
. In this paper we present a program specialisation which, given a call/post specification, transforms a logic program into a callcorrect one satisfying the post-condition. The specialisation is applied to specialised partially correct programs. This notion is based on the definition of specialised derivation which is intended to describe program behaviour whenever some properties on procedure calls are assumed. Operational and fixpoints semantics modeling specialised derivations are recalled. We show on an example how our program specialisation constitutes a first step transformation versus an effective program optimization. 1 Introduction Specialisation methods allow one to restrict a program to a narrower...
New Ideas for Solving Covering Problems
- Olivier Coudert; Jean Christophe Madre
Covering problems occur at several steps during logic synthesis including two-level minimization and DAG covering. This paper presents a better lower bound computation algorithm and two new pruning techniques that significantly improve the efficiency of covering problem solvers. We show that these techniques reduce by up to three orders of magnitude the time required to solve covering problems exactly. 1 Introduction The (unate or binate) covering problem is a well known intractable problem. It has several important applications in logic synthesis, such as two-level logic minimization, two-level Boolean relation minimization, three-level NAND implementation, state minimization, exact encoding, and DAG covering...
Temporal Conditions and Integrity Constraints in Active Database Systems
- A. Prasad Sistla; Ouri Wolfson
In this paper, we present a unified formalism, based on Past Temporal Logic, for specifying conditions and events in the rules for active database system. This language permits specification of many time varying properties of database systems. It also permits specification of temporal aggregates. We present an efficient incremental algorithm for detecting conditions specified in this language. The given algorithm, for a subclass of the logic, was implemented on top of Sybase. 0 1 Introduction The most popular model of rules in active database systems is the ECA model [41, 6, 28, 5, 14, 18]. It defines a rule to...
Specification Enforcing Refinement for Convertibility Verification
- Partha S Roop; Alain Girault; Roopak Sinha; Gregor Goessler
Abstract—Protocol conversion deals with the automatic syn-thesis of an additional component or glue logic, often referred to as an adaptor or an interface, to bridge mismatches between interacting components, often referred to as protocols. A formal solution, called convertibility verification, has been recently proposed, which produces such a glue logic, termed as a converter, so that the parallel composition of the protocols and the converter also satisfies some desired specification. A converter is responsible for bridging different kinds of mismatches such as control, data, and clock mismatches. Mismatches are usually removed by the converter (similar to controllers in supervisory control...
Exploring Overlaps and Differences in Service Dominant Logic and Design Thinking Katar ina Wet t e r Edman Katarina Wetter Edman PhD Candidate, MFA Industrial Design Business and Design Lab
- Hdk/school Of Business
Design tradition takes the user as a starting point and focuses on his or her needs, wants and expectations. Recently, within the service marketing/management area, the user has been highlighted not only as “the king”, but as the only one to determine value. This new logic is termed Service Dominant Logic. Some of the key principles underlying Service Dominant Logic (SDL) and Design Thinking (DT) are strikingly similar. Even if the two concepts stem from different backgrounds, both are deeply concerned with the creation of value and the importance of understanding the users/customers. This similarity could be a fruitful ground...
Anti-CD45 Monoclonal Antibody YAML568: A Promising Radioimmunoconjugate for Targeted Therapy of Acute Leukemia
- Gerhard Glatting; Bernd Koop; Kathrin Hohl; Claudia Friesen; Bernd Neumaier; Eleanor Berrie; Pru Bird; Geoffrey Hale; Norbert M. Blumstein; Herman Waldmann; Donald Bunjes; Sven N. Reske
The outcome of hematopoietic cell transplantation for hemato-logic malignancies may be improved by delivering targeted radi-ation to hematopoietic organs while relatively sparing nontarget organs. We evaluated the biodistribution of 111In-labeled anti-CD45 antibody in humans using the rat IgG2a monoclonal anti-body YAML568 that recognizes a common CD45 epitope present on all human leukocytes. Methods: Eight patients un-dergoing bone marrow transplantation received YAML568 la-beled with 122 6 16 MBq of 111In intravenously followed by serial blood sampling, urine collection, and conjugated view pla-nar g-camera imaging up to 144 h after injection. Time–activity curves were obtained using region-of-interest analysis in the ac-cumulating organs...