
Fahiem Bacchus
We present a mechanism for constructing graphical models, speci cally Bayesian networks, from a knowledge base of general probabilistic information. The unique feature of our approach is that it uses a powerful firstorder 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 wewant toreason about. These pieces are composed to generate a joint probability distribution specified...

P. Lópezgarcía; F. Bueno; M. Hermenegildo
Abstract. We propose an analysis for detecting procedures and goals that are deterministic (i.e. that produce at most one solution), or predicates whose clause tests are mutually exclusive (which implies that at most one of their clauses will succeed) even if they are not deterministic (because they call other predicates that can produce more than one solution). Applications of such determinacy information include detecting programming errors, performing certain highlevel program transformations for improving search efficiency, optimizing low level code generation and parallel execution, and estimating tighter upper bounds on the computational costs of goals and data sizes, which can be...

Jérôme Thoméré; Ken Barker; Vinay Chaudhri; Peter Clark; Michael Eriksen; Bruce Porter; Andres Rodriguez
Making logicbased AI representations accessible to ordinary users has been an ongoing challenge for the successful deployment of knowledge bases. Past work to meet this objective has resulted in a variety of ontology editing tools and taskspecific knowledgeacquisition methods. In this paper, we describe a Webbased ontology browsing and editing system with the following features: (a) wellorganized Englishlike presentation of concept descriptions and (b) use of graphs to enter concept relationships, add/delete lists, and analogical correspondences. No existing tool supports these features. The system is Webbased and its user interface uses a mixture of HTML and Java. It has undergone...

Tommaso Di Noia; Eugenio Di Sciascio; Francesco M. Donini
Matchmaking arises when supply and demand meet in an electronic marketplace, or when agents search for a web service to perform some task, or even when recruiting agencies match curricula and job profiles. In such open environments, the objective of a matchmaking process is to discover best available offers to a given request. We address the problem of matchmaking from a knowledge representation perspective, with a formalization based on Description Logics. We devise Concept Abduction and Concept Contraction as nonmonotonic inferences in Description Logics suitable for modeling matchmaking in a logical framework, and prove some related complexity results. We also...

Current dynamic epistemic logics for analyzing effects of informational events often become cumbersome and opaque when common knowledge is added for groups of agents. Still, postconditions involving common knowledge are essential to successful multiagent communication. We propose new systems that extend the epistemic base language with a new notion of ‘relativized common knowledge’, in such a way that the resulting full dynamic logic of information flow allows for a compositional analysis of all epistemic postconditions via perspicuous ‘reduction axioms’. We also show how such systems can deal with factual alteration, rather than just information change, making them cover a much...

Y. A. Skobtsov; D. E. Ivanov; V. Y. Skobtsov; R. Ubar; J. Raik
In the paper, an evolutionary approach to test generation for functional BIST is considered. The aim of the proposed scheme is to minimize the test data volume by allowing the device’s microprogram to test its logic, providing an observation structure to the system, and generating appropriate test data for the given architecture. Two methods of deriving a deterministic test set at functional level are suggested. The first method is based on the classical genetic algorithm with binary and arithmetic crossover and mutation operators. The second one uses genetic programming, where test is represented as a sequence of microoperations. In the...

Antonino Salibra
The author wishes to thank Istvan for his teachings over these years Abstract. The untyped lambda calculus was introduced around 1930 by Church as part of an investigation in the formal foundations of mathematics and logic. Although lambda calculus is a very basic language, it is sufficient to express all the computable functions. The process of application and evaluation reflects the computational behaviour of many modern functional programming languages, which explains the interest in the lambda calculus among computer scientists. In this paper we give an outline of the theory of lambda abstraction algebras (LAA’s). These algebras constitute an equational...

Matteo Baldoni; Advisor Prof; Alberto Martelli; Coadvisor Dr. Laura Giordano
In this thesis we work on normal multimodal logics, that are general modal systems with an arbitrary set of normal modal operators, focusing on the class of inclusion modal logics. This class of logics, first introduced by Fariñas del Cerro and Penttonen, includes some wellknown nonhomogeneous multimodal systems characterized by interaction axioms of the form [t1][t2]... [tn]ϕ ⊃ [s1][s2]... [sm]ϕ, that we call inclusion axioms. The thesis is organized in two part. In the first part the class of inclusion modal logics is deeply studied by introducing the the syntax, the possibleworlds semantics, and the axiomatization. Afterwards, we define a...

Abstract – A modeling approach is presented that captures the dependence of the power dissipation of a combinational logic circuit on its input/output signal switching activity. The resulting power macromodel, consisting of a single three dimensional table, can be used to estimate the power consumed in the circuit for any given input/output signal statistics. Given a lowlevel (typically gatelevel) description of the circuit, we describe a characterization process by which such a table model can be automatically built. In contrast to other proposed techniques, this can be done for any given logic circuit without any user intervention, and applies to...

Norman L. Johnson; Kerstin Dautenhahn
Following a nonreductionist approach to the explanation of higher functionality observed in collective problem solvers, a simple agentbased model is used to “solve ” a sequential problem a maze. Larger collectives of the individual agents are observed in the simulations to locate a minimal path, even though the agents are noninteracting, have no global perception of the maze and use rules that do not include logic for finding a shorter path. The convergence to an optimal path is argued to be a demonstration of both an emergent problem formulation and emergent problem solution. Furthermore, many of the dynamics and properties...

Du Li, et al.
COCA (Collaborative Objects Coordination Architecture) was proposed as a novel means to model and support collaborations over the Internet. Our approach separates coordination policies from user interfaces and the policies are specified in a logicbased language. Over the past year, both the collaboration model and the specification language have been substantially refined and evaluated through our experience in building reallife collaboration systems. This paper presents the design of the specification language and illustrates the main ideas with a few simple design examples. Semantics, implementation, runtime support, and applications are also covered but not as the focus of this paper.

Irène Guessarian; Jeaneric Pin
We give in this paper a sufficient condition under which the least fixpoint of the equation X = a + f(X)X equals the least fixpoint of the equation X = a + f(a)X. We then apply that condition to recursive logic programs containing chain rules: we translate it into a sufficient condition under which a recursive logic program containing n ≥ 2 recursive calls in the bodies of the rules is equivalent to a linear program containing at most one recursive call in the bodies of the rules. We conclude with a discussion comparing our condition with the other approaches...

In this work, we present a syndication framework in which Description Logic (DL) reasoning is used for matching subscription requests with newly published information. One of the main limitations of previous efforts is related to the poor scalability of DL reasoners, especially when handling updates. This has made a DL based approach impractical for syndication of time sensitive information. To overcome this, the presented framework leverages recent work on incremental reasoning through changes of ontologies, thereby making such a system more appropriate for such applications. 1

Quoc Bao Vo; Norman Y. Foo
We present a uniform nonmonotonic solution to the problems of reasoning about action on the basis of an argumentationtheoretic approach. Our theory is provably correct relative to a sensible minimisation policy introduced on top of a temporal propositional logic. Sophisticated problem domains can be formalised in our framework. As much attention of researchers in the field has been paid to the traditional and basic problems in reasoning about actions such as the frame, the qualification and the ramification problems, approaches to these problems within our formalisation lie at heart of the expositions presented in this paper. 1.

Paul F. Syverson
We present a logic for analyzing cryptographic protocols. This logic encompasses a uni cation of four of its predecessors in the BAN family of logics, namely those given in [GNY90], [AT91], [vO93], and BAN itself [BAN89]. We also present a modeltheoretic semantics with respect to which the logic is sound. The logic herein captures all of the desirable features of its predecessors and more; nonetheless, it accomplishes this with no more axioms or rules than the simplest of its predecessors.

Ádám Darvas, et al.
Most attempts at analysing secure information flow in programs are based on domainspecific logics. Though computationally feasible, these approaches suffer from the need for abstraction and the high cost of building dedicated tools for real programming languages. We recast the information flow problem in a general program logic rather than a problemspecific one. We investigate the feasibility of this approach by showing how a general purpose tool for software verification can be used to perform information flow analyses. We are able to handle phenomena like method calls, loops, and object types for the target language Java Card. We are also...

Emmanuel Coquery; François Fages; Université Claude; Bernard Lyon
Abstract. We propose a generic type system for the Constraint Handling Rules (CHR), a rewriting rule language for implementing constraint solvers. CHR being a highlevel extension of a host language, such as Prolog or Java, this type system is parameterized by the type system of the host language. We show the consistency of the type system for CHR w.r.t. its operational semantics. We also study the case when the host language is a constraint logic programming language, typed with the prescriptive type system we developed in previous work. In particular, we show the consistency of the resulting type system w.r.t....

Compilation to boolean satisfiability has become a powerful paradigm for solving AI problems. However, domains that require metric reasoning cannot be compiled efficiently to SAT even if they would otherwise benefit from compilation. We address this problem by introducing the lcnf representation which combines propositional logic with metric constraints. We present lpsat, an engine which solves lcnf problems by interleaving calls to an incremental simplex algorithm with systematic satisfaction methods. We describe a compiler which converts metric resource planning problems into lcnf for processing by lpsat. The experimental section of the paper explores several optimizations to lpsat, including learning from...

We develop a model of normative systems in which agents are assumed to have multiple goals of increasing priority, and investigate the computational complexity and game theoretic properties of this model. In the underlying model of normative systems, we use Kripke structures to represent the possible transitions of a multiagent system. A normative system is then simply a subset of the Kripke structure, which contains the arcs that are forbidden by the normative system. We specify an agent’s goals as a hierarchy of formulae of Computation Tree Logic (CTL), a widely used logic for representing the properties of Kripke structures:...

Koushik Sen; Mahesh Viswanathan; Gul Agha
Abstract. Statistical methods to model check stochastic systems have been, thus far, developed only for a sublogic of continuous stochastic logic (CSL) that does not have steady state operators and unbounded until formulas. In this paper, we present a statistical model checking algorithm that also verifies CSL formulas with unbounded untils. The algorithm is based on Monte Carlo simulation of the model and hypothesis testing of the samples, as opposed to sequential hypothesis testing. The use of statistical hypothesis testing allows us to exploit the inherent parallelism in this approach. We have implemented the algorithm in a tool called VESTA,...