281.

A Proof Theory for Constructive Default Logic
- Yao-hua Tan
. We present what we call Constructive Default Logic (CDL) - a default logic in which the fixedpoint definition of extensions is replaced by a constructive definition which yield so-called constructive extensions. Selection functions are used to represent explicitly the control of the reasoning process in this default logic. It is well-known that Reiter's original default logic lacks, in general, a default proof theory. We will show that CDL does have a default proof theory, and we will also show that this is related to the fact that CDL has the existence property for constructive extensions and that it also...

282.

Real Time Systems: A Tutorial
- F. Panzieri; R. Davoli
s are available from the same host in the directory /pub/TR/UBLCS/ABSTRACTS in plain text format. All local authors can be reached via e-mail at the address last-name@cs.unibo.it. UBLCS Technical Report Series 93-1 Consistent Global States of Distributed Systems: Fundamental Concepts and Mechanism, by O. Babao glu and K. Marzullo, January 1993. 93-2 Understanding Non-Blocking Atomic Commitment, by O. Babao glu and S. Toueg, January 1993. 93-3 Anchors and Paths in a Hypertext Publishing System, by C. Maioli and F. Vitali, February 1993. 93-4 A Formalization of Priority Inversion, by O. Babao glu, K. Marzullo and F. Schneider, March 1993. 93-5...

283.

Combining Petri Nets and PA-Processes
- Richard Mayr
Petri nets and PA-processes are incomparable models of infinite state concurrent systems. We define a new model PAN (= PA + PN) that subsumes both of them and is thus strictly more expressive than Petri nets. It extends Petri nets with the possibility to call subroutines. We show that the reachability problem is still decidable for PAN. It is even decidable, if there is a reachable state that satisfies certain properties that can be encoded in a simple logic.

284.

A Davis-Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems
- William Mccune Mathematics; William Mccune
This document describes the implementation and use of a Davis-Putnam procedure for the propositional satisfiability problem. It also describes code that takes statements in firstorder logic with equality and a domain size n searches for models of size n. The first-order model-searching code transforms the statements into set of propositional clauses such that the first-order statements have a model of size n if and only if the propositional clauses are satisfiable. The propositional set is then given to the Davis-Putnam code; any propositional models that are found can be translated to models of the first-order statements. The firstorder model-searching program...

285.

Lp, A Logic for Representing and Reasoning with Statistical Knowledge
- Fahiem Bacchus
This paper presents a logical formalism for representing and reasoning with statistical knowledge. One of the key features of the formalism is its ability to deal with qualitative statistical information. It is argued that statistical knowledge, especially that of a qualitative nature, is an important component of our world knowledge and that such knowledge is used in many different reasoning tasks. The work is further motivated by the observation that previous formalisms for representing probabilistic information are inadequate for representing statistical knowledge. The representation mechanism takes the form of a logic that is capable of representing a wide variety of...

286.

Using First-Order Probability Logic for the Construction of Bayesian Networks
- Fahiem Bacchus
We present a mechanism for constructing graphical models, specifically Bayesian networks, from a knowledge base of general probabilistic information. The unique feature of our approach is that it uses a powerful first-order probabilistic logic for expressing the general knowledge base. This logic allows for the representation of a wide range of logical and probabilistic information. The model construction procedure we propose uses notions from direct inference to identify pieces of local statistical information from the knowledge base that are most appropriate to the particular event we want to reason about. These pieces are composed to generate a joint probability distribution...

287.

Structural Operational Semantics for AKL
- Seif Haridi; Sverker Janson; Catuscia Palamidessi
The Andorra Kernel Language (AKL) is a concurrent constraint programming language. It can be seen as a general combination of logic programming languages such as Prolog, GHC, and Parlog, the first of which provides don't know nondeterminism, and the last two of which are concurrent logic programming languages. The constraint system is an independent parameter of the language description. In this paper, we revisit the description of Janson and Haridi [10], adding the formal machinery which is necessary in order to completely formalize the control of the computation model. To this we add a formal description of the transformational semantics...

288.

PARCS: An MPP-Oriented CLP Language
- Kazuhiro Konno; Nagatsuka Masaaki; Naoki KOBAYASHI; Matsuoka Satoshi; Yonezawa Akinori
: PARCS is a declarative parallel constraint logic programming (CLP) language designed for efficient execution on distributed memory massively parallel processors (MPPs). As a language model, PARCS offers efficient parallel execution control via priority-based goal and constraint execution, powerful pruning mechanisms, and implicit OR-parallelism. Its MPPoriented implementation techniques include efficient load balancing, branching method and static compile-time optimization techniques such as mode-specific code generation, static ordering of deterministic constraints and determinacy analysis. Actual experiments have shown good speedups with respect to the number of processors for various kinds of programs, such as N-queens and paraffin problem. Keywords: constraint logic programming,...

289.

Embedding extensional finite sets in CLP
- Agostino Dovier; Gianfranco Rossi
In this paper we review the definition of {log}, a logic language with sets, from the viewpoint of CLP. We show that starting with a CLP-scheme allows a more uniform treatment of the built-in set operations (namely, =, 2 and their negative counterparts), and allows all the theoretical results of CLP to be immediately exploitable. We prove this by precisely defining the privileged interpretation domain and the axioms of the selected set theory. Then we define a non-deterministic procedure for checking constraint satisfiability based on the reduction of a given constraint to a collection of constraint in a suitable canonical...

290.

Knowledge Acquisition From Complex Domains By Combining Inductive Learning and Theory Revision
- Xiaolong Zhang; Xiaolong Zhang; Masayuki Numao; Masayuki Numao
In the process of knowledge acquisition, inductive learning and theory revision play important roles. Inductive learning is used to acquire new knowledge (theories) from training examples; and theory revision improves an initial theory with training examples. A theory preference criterion is critical in the processes of inductive learning and theory revision. A new system called knowar is developed by integrating inductive learning and theory revision. In addition, the theory preference criterion used in knowar is the combination of the MDL-based heuristic and the Laplace estimate. The system can be used to deal with complex problems. Empirical studies have confirmed that...

291.

Zooming In, Zooming Out
- Patrick Blackburn; Maarten De Rijke
. In Journal of Logic, Language and Information, to appear. This is an exploratory paper about combining logics, combining theories and combining structures. Typically when one applies logic to such areas as computer science, artificial intelligence or linguistics, one encounters hybrid ontologies. The aim of this paper is to identify plausible strategies for coping with ontological richness. Key words: Combinations of logics, complex structures, mathematics of modeling, modularity, modal logic, representation languages, transfer results AMS Subject Classification (1991): 00A71, 03B45 CR Subject Classification (1991): F.4.0, F.4.1, I.2.4 1. Day 1: Examples Zi: There's only two things I want to say:...

292.

Computing Argumentation in Logic Programming
- Antonios C. Kakas; Francesca Toni
In recent years, argumentation has been shown to be an appropriate framework in which logic programming with negation as failure as well as other logics for non-monotonic reasoning can be encompassed. Many of the existing semantics for negation as failure in logic programming can be understood in a uniform way using argumentation. Moreover, other logics for non-monotonic reasoning that can also be formulated via argumentation can be given new semantics, by a direct extension of the logic programming semantics. In this paper we develop an abstract computational framework where various argumentation semantics can be computed via different parametric variations of...

293.

Distributed Semantic Query Processing in a Cooperative Information System
- John Cardiff; Tiziana Catarci; Giuseppe Santucci
Visual Query System (VQS) is a suitable interface to a cooperative information system, as its users often have no knowledge of the structure or location of the data. However queries issued through a VQS may be translated into inefficient queries to the component systems, if the semantics of the system are not considered. In this paper, we present the design of a semantic query preprocessor for a cooperative information system. We also introduce a logic language to formally express interdependencies between classes belonging to different schemas. Using these assertions, we may benefit in several ways from the possibility of reasoning...

294.

Evaluating First Order Formulas - the foundation for a general Search Engine
- Fahiem Bacchus; Michael Ady
Search and declarative representations are two of the most important themes in AI research. Many problems in AI require search for their solution, and declarative representations of the knowledge required to solve these problems offer many advantages. In this paper we show how these two themes can be combined. In particular, we show how a general search engine can be designed that is based on the most familiar declarative representation: first order logic. The system can be used to solve both search problems and optimization problems, e.g., job-shop scheduling, as well as problems traditionally viewed as being planning problems, e.g.,...

295.

Process Rewrite Systems
- Richard Mayr
Many formal models for infinite-state concurrent systems are equivalent to special classes of rewrite systems. We classify these models by their expressiveness and define a hierarchy of classes of rewrite systems. We show that this hierarchy is strict with respect to bisimulation equivalence. The most general and most expressive class of systems in this hierarchy is called Process Rewrite Systems (PRS). They subsume Petri nets, PA-Processes and pushdown processes and are strictly more expressive than any of these. Intuitively, PRS can be seen as an extension of Petri nets by subroutines that can return a value to their caller. We...

296.

Search-Space Pruning Heuristics for Path Sensitization in Test Pattern Generation
- Joao P. Marques-Silva; Jo��o P. Marques Silva; Jo��o P. Marques Silva; Karem A. Sakallah; Karem A. Sakallah
A powerful combinational path sensitization engine is required for the efficient implementation of tools for test pattern generation, timing analysis, and delay-fault testing. Path sensitization can be posed as a search, in the ndimensional Boolean space, for a consistent assignment of logic values to the circuit nodes which also satisfies a given condition. While the conditions for path sensitization are different for different applications, the search mechanism need not be. In this paper we propose and demonstrate the effectiveness of several new deterministic techniques for search-space pruning for test pattern generation. These techniques are based on a dynamic analysis of...

297.

Inductive Constraint Logic and the Mutagenesis Problem
- Hendrik Blockeel; Wim Van Laer; Luc De Raedt
A novel approach to learning first order logic formulae from positive and negative examples is incorporated in a system named ICL (Inductive Constraint Logic). In ICL, examples are viewed as interpretations which are true or false for the target theory, whereas in present inductive logic programming systems, examples are true and false ground facts (or clauses). Furthermore, ICL uses a clausal representation, which corresponds to a conjunctive normal form where each conjunct forms a constraint on positive examples, whereas classical learning techniques have concentrated on concept representations in disjunctive normal form. We present some experiments with this new system on...

298.

Tractable and Decidable Fragments of Conceptual Graphs
- Franz Baader; Ralf Molitor; Stephan Tobies
It is well-known that problems like validity and subsumption of general CGs are undecidable, whereas subsumption is NP-complete for simple conceptual graphs (SGs) and tractable for SGs that are trees. We will employ results on decidable fragments of rst-order logic to identify a natural and expressive fragment of CGs for which validity and subsumption is decidable in ExpTime. In addition, we will extend existing work on the connection between SGs and description logics (DLs) by identifying a DL that corresponds to the class of SGs that are trees. This yields a tractability result previously unknown in the DL community.

299.

Hints to Specifiers
- Jeannette M. Wing
I present a list of hints for writing specifications. I address high-level issues like learning to abstract and low-level issues like getting the details of logical expressions right. This paper should be of interest not only to students of formal methods but also to their teachers. This research is sponsored by the Wright Laboratory, Aeronautical Systems Center, Air Force Materiel Command, USAF, and the Advanced Research Projects Agency (ARPA) under grant number F33615-93-1-1330. Views and conclusions contained in this document are those of the authors and should not be interpreted as necessarily representing official policies or endorsements, either expressed or...

300.

Why Are Modal Logics So Robustly Decidable?
- Erich Grädel
Modal logics are widely used in a number of areas in computer science, in particular for the specification and verification of hardware and software systems, for knowledge representation, in databases, and in artificial intelligence. The most important reason for the successful applications of these logics is that they provide a good balance between expressive power and computational complexity. In [30] Vardi adressed the question to identify the main reasons for the robust decidability properties of modal logics. In particular he stressed the importance of the tree model property, which permits the use of powerful automata-theoretic techniques. Here we discuss this...