This paper further introduces and formalizes a novel concept of self-forensics for automotive vehicles, specified in the Forensic Lucid language. We argue that self-forensics, with the forensics taken out of the cybercrime domain, is applicable to "self-dissection" of intelligent vehicles and hardware systems for automated incident and anomaly analysis and event reconstruction by the software with or without the aid of the engineering teams in a variety of forensic scenarios. We propose a formal design, requirements, and specification of the self-forensic enabled units (similar to blackboxes) in vehicles that will help investigation of incidents and also automated reasoning and verification of theories along with the events reconstruction in a formal model. We argue such an analysis is beneficial to improve the safety of the passengers and their vehicles, like the airline industry does for planes.

We present a straightforward embedding of quantified multimodal logic in simple type theory and prove its soundness and completeness. Modal operators are replaced by quantification over a type of possible worlds. We present simple experiments, using existing higher-order theorem provers, to demonstrate that the embedding allows automated proofs of statements in these logics, as well as meta properties of them.

We present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/non-termination proof approaches. We introduce an idea of termination prediction, which predicts termination of a logic program in case that neither a termination nor a non-termination proof is applicable. We establish a necessary and sufficient characterization of infinite (generalized) SLDNF-derivations with arbitrary (concrete or moded) queries, and develop an algorithm that predicts termination of general logic programs with arbitrary non-floundering queries. We have implemented a termination prediction tool and obtained quite satisfactory experimental results. Except for five programs which break the experiment time limit, our prediction is 100% correct for all 296 benchmark programs of the Termination Competition 2007, of which eighteen programs cannot be proved by any of the existing state-of-the-art analyzers like AProVE07, NTI, Polytool and TALP.

This paper studies the stable model semantics of logic programs with (abstract) constraint atoms and their properties. We introduce a succinct abstract representation of these constraint atoms in which a constraint atom is represented compactly. We show two applications. First, under this representation of constraint atoms, we generalize the Gelfond-Lifschitz transformation and apply it to define stable models (also called answer sets) for logic programs with arbitrary constraint atoms. The resulting semantics turns out to coincide with the one defined by Son et al., which is based on a fixpoint approach. One advantage of our approach is that it can be applied, in a natural way, to define stable models for disjunctive logic programs with constraint atoms, which may appear in the disjunctive head as well as in the body of a rule. As a result, our approach to the stable model semantics for logic programs with constraint atoms generalizes a number of previous approaches. Second, we show that our abstract representation of constraint atoms provides a means to characterize dependencies of atoms in a program with constraint atoms, so that some standard characterizations and properties relying on these dependencies in the past for logic programs with ordinary atoms can be extended to logic programs with constraint atoms.

This papers develops a logical language for representing probabilistic causal laws. Our interest in such a language is twofold. First, it can be motivated as a fundamental study of the representation of causal knowledge. Causality has an inherent dynamic aspect, which has been studied at the semantical level by Shafer in his framework of probability trees. In such a dynamic context, where the evolution of a domain over time is considered, the idea of a causal law as something which guides this evolution is quite natural. In our formalization, a set of probabilistic causal laws can be used to represent a class of probability trees in a concise, flexible and modular way. In this way, our work extends Shafer's by offering a convenient logical representation for his semantical objects. Second, this language also has relevance for the area of probabilistic logic programming. In particular, we prove that the formal semantics of a theory in our language can be equivalently defined as a probability distribution over the well-founded models of certain logic programs, rendering it formally quite similar to existing languages such as ICL or PRISM. Because we can motivate and explain our language in a completely self-contained way as a representation of probabilistic causal laws, this provides a new way of explaining the intuitions behind such probabilistic logic programs: we can say precisely which knowledge such a program expresses, in terms that are equally understandable by a non-logician. Moreover, we also obtain an additional piece of knowledge representation methodology for probabilistic logic programs, by showing how they can express probabilistic causal laws.

Semantic web services (SWS) are self-contained, self-describing, semantically marked-up software resources that can be published, discovered, composed and executed across the Web in a semi-automatic way. They are a key component of the future Semantic Web, in which networked computer programs become providers and users of information at the same time. This work focuses on developing a full-life-cycle software toolset for creating and maintaining Semantic Web Services (SWSs) based on the Web Service Modelling Ontology (WSMO) framework. A main part of WSMO-based SWS is service capability - a declarative description of Web service functionality. A formal syntax and semantics for such a description is provided by Web Service Modeling Language (WSML), which is based on different logical formalisms, namely, Description Logics, First-Order Logic and Logic Programming. A WSML description of a Web service capability is represented as a set of complex logical expressions (axioms). We develop a specialized user-friendly tool for constructing and editing WSMO-based SWS capabilities. Since the users of this tool are not specialists in first-order logic, a graphical way for constricting and editing axioms is proposed. The designed process for constructing logical expressions is ontology-driven, which abstracts away as much as possible from any concrete syntax of logical language. We propose several mechanisms to guarantees the semantic consistency of the produced logical expressions. The tool is implemented in Java using Eclipse for IDE and GEF (Graphical Editing Framework) for visualization.

The theme of this article is the dynamics of evolution of agents. That theme is applied to the evolution of constraint satisfaction, of agents themselves, of our models of agents, of artificial intelligence and, finally, of the Association for the Advancement of Artificial Intelligence (AAAI). The overall thesis is that constraint satisfaction is central to proactive and responsive intelligent behavior.

In this paper, we investigate the deductive inference for the interiors and exteriors of Horn knowledge bases, where the interiors and exteriors were introduced by Makino and Ibaraki to study stability properties of knowledge bases. We present a linear time algorithm for the deduction for the interiors and show that it is co-NP-complete for the deduction for the exteriors. Under model-based representation, we show that the deduction problem for interiors is NP-complete while the one for exteriors is co-NP-complete. As for Horn envelopes of the exteriors, we show that it is linearly solvable under model-based representation, while it is co-NP-complete under formula-based representation. We also discuss the polynomially solvable cases for all the intractable problems.

The management and combination of uncertain, imprecise, fuzzy and even paradoxical or high conflicting sources of information has always been, and still remains today, of primal importance for the development of reliable modern information systems involving artificial reasoning. In this introduction, we present a survey of our recent theory of plausible and paradoxical reasoning, known as Dezert-Smarandache Theory (DSmT), developed for dealing with imprecise, uncertain and conflicting sources of information. We focus our presentation on the foundations of DSmT and on its most important rules of combination, rather than on browsing specific applications of DSmT available in literature. Several simple examples are given throughout this presentation to show the efficiency and the generality of this new approach.

We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic -- in our case a sequent calculus for classical type theory -- is like adding cut. The phenomenon equally applies to prominent axioms like Boolean- and functional extensionality, induction, choice, and description. This calls for the development of calculi where these principles are built-in instead of being treated axiomatically.