Search

We propose a simple and efficient approach to the verification of parameterized and infinite state system. The approach is based on modeling the reachability relation between parameterized states as deducibility between suitable encodings of the states using formulae of first-order logic. To establish a safety property, namely the non-reachability of unsafe states, a finite model finder is used to generate a finite countermodel, thus providing the witness for non-deducibility. We show that under an appropriate encoding the combination of finite model finding and theorem proving provides us with a decision procedure for the safety of the lossy channel systems. We illustrate the approach by reporting on experiments verifying both alternating bit protocol (specified as a lossy channel system) and a number of parameterized cache coherence protocols specified by extended finite state machines. In these experiments, the finite model finder Mace4 is used. [ABSTRACT FROM AUTHOR]

The automated verification of concurrent and distributed systems is a vibrant and successful area within Computer Science. Over the last 30 years, temporal logic [10,20] has been shown to provide a clear, concise and intuitive description of many such systems, and automata-theoretic techniques such as model checking [7,14] have been shown to be very useful in practical verification. Recently, the verification of infinite-state systems, particularly parameterised systems comprising arbitrary numbers of identical processes, has become increasingly important [5]. Practical problems of an open, distributed nature often fit into this model, for example robot swarms of arbitrary sizes. [ABSTRACT FROM AUTHOR]

In this paper we investigate the computational complexity of knot theoretic problems and show upper and lower bounds for planarity problem of signed and unsigned knot diagrams represented by Gauss words. Due to the fact the number of crossing in knots is unbounded, the Gauss words of knot diagrams are strings over infinite (unbounded) alphabet. For establishing the lower and upper bounds on recognition of knot properties we study these problems in a context of automata models over infinite alphabet. [ABSTRACT FROM AUTHOR]

Given a program with two arguments p(x,y). Let the first argument x0 be fixed. The aim of program specialization with respect to the known x0 is to construct an optimized program Px0(y) such that Px0(y) = P(x0,y). Specialization of interpreters with respect to programs is well known problem. In this paper we argue that specialization of interpreters with respect to data may be seen as program verification. [ABSTRACT FROM AUTHOR]

This work is a contribution to realizing prioritized reasoning in logic programming in the presence of preference relations involving atoms. In more details, the case of dynamic preferences is investigated and a semantics interpreting each preference rule as a tool for representing a choice over alternative options is proposed. The technique, providing a new interpretation for prioritized logic programs, is inspired by the one proposed by Sakama and Inoue in [19] and enriched with the use of structural information of preference rules as proposed by Brewka et al. in [6]. Specifically, the analysis of the logic program is carried out together with the analysis of preferences in order to determine the choice order and the sets of comparable models. The proposed approach is compared with those in [6, 19]. Complexity analysis is also performed showing that the use of additional information does not increase the complexity of computing preferred stable models. [ABSTRACT FROM AUTHOR]

n-tableaux [1] and δ-resolution [2], which are based, respectively, on semantic tableaux and resolution, have been properly used for the resolution of abductive problems. The tool we present is a Prolog implementation of an abductive solver which combines both calculi to attack first order abductive problems by reducing them to finite versions, that is, propositional rewritings of the problems which presuppose a context representable with finite models with a known cardinality. [ABSTRACT FROM AUTHOR]

We consider action domain descriptions whose meaning can be represented by transition diagrams. We introduce several semantic measures to compare such action descriptions, based on preferences over possible states of the world and preferences over some given conditions (observations, assertions, etc.) about the domain, as well as the probabilities of possible transitions. This preference information is used to assemble a weight which is assigned to an action description. As an application of this approach, we study the problem of updating action descriptions with respect to some given conditions. With a semantic approach based on preferences, not only, for some problems, we get more plausible solutions, but also, for some problems without any solutions due to too strong conditions, we can identify which conditions to relax to obtain a solution. We conclude with computational issues, and characterize the complexity of computing the semantic measures. [ABSTRACT FROM AUTHOR]

The theory of arrays, introduced by McCarthy in his seminal paper "Toward a mathematical science of computation", is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e. checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays has the algebraic structure of Presburger Arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger Arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i.e., superposition) techniques to implement the instantiation strategies of the various extensions. [ABSTRACT FROM AUTHOR]

Computationally adequate representation of models is a topic arising in various forms in logic and AI. Two fundamental decision problems in this area are: (1) to check whether a given clause is true in a represented model, and (2) to decide whether two representations of the same type represent the same model. ARMs, contexts and DIGs are three important examples of model representation formalisms. The complexity of the mentioned decision problems has been studied for ARMs only for finite signatures, and for contexts and DIGs only for infinite signatures, so far. We settle the remaining cases. Moreover we show that, similarly to the case for infinite signatures, contexts and DIGs allow one to represent the same classes of models also over finite signatures; however DIGs may be exponentially more succinct than all equivalent contexts. [ABSTRACT FROM AUTHOR]

We present a general method to formalize action domains with numeric-valued fluents whose values are incremented or decremented by executions of actions, and show how it can be applied to the action description language $\cal C+$ and to the concurrent situation calculus. This method can handle nonserializable concurrent actions, as well as ramifications on numeric-valued fluents, which are described in terms of some new causal structures, called contribution rules. [ABSTRACT FROM AUTHOR]

Recognizing and extracting meaningful information from unstructured Web documents, taking into account their semantics, is an important problem in information and knowledge management. This paper describes H$\imath$LεX, a system implementing a novel logic-based approach to information extraction from unstructured documents. The approach adopted in the H$\imath$LεX system is founded on a new two-dimensional representation of documents, and heavily exploits DLP+ - an extension of disjunctive logic programming for ontology representation and reasoning, which has been recently implemented on top of the DLV system. Unlike previous systems, which are mainly syntactic, H$\imath$LεX combines both semantic and syntactic knowledge for a powerful information extraction. Ontologies, representing the semantics of the domain of the information to be extracted, are encoded in DLP+, while the extraction patterns are encoded by regular expressions in an ad hoc two-dimensional grammar. These regular expressions are (internally) translated into DLP+ rules, whose execution yields the actual extraction of information from the input document. H$\imath$LεX allows the semantic information extraction from both HTML pages and flat text documents. The usefulness of Hilex has been already confirmed also in practice, as the system has been successfully employed in two advanced applications in the e-health and e-finance domains. [ABSTRACT FROM AUTHOR]

In recent work, a general framework for specifying correspondences between logic programs under the answer-set semantics has been defined. The framework captures different notions of equivalence, including well-known ones like ordinary, strong, and uniform equivalence, as well as refined ones based on the projection of answer sets where not all parts of an answer set are of relevance. In this paper, we describe an implementation to verify program correspondences in this general framework. The system, called cc$\top$, relies on linear-time constructible reductions to quantified propositional logic and uses extant solvers for the latter language as back-end inference engines. [ABSTRACT FROM AUTHOR]

Program slicing is a well-known technique that has been widely used for debugging in the context of imperative programming. Debugging is a particularly difficult task within lazy declarative programming. In particular, there exist very few approaches to program slicing in this context. In this paper, we describe a slicing tool for first-order lazy functional logic languages. We also illustrate its usefulness by means of an example. [ABSTRACT FROM AUTHOR]

In this paper we describe the QBFEVAL web portal, an on-line resource supporting the participants and the organizers of the yearly evaluation of QBF solvers and instances. [ABSTRACT FROM AUTHOR]

In this paper we compare two approaches to automated reasoning about metric and topology in the framework of the logic $\mathcal{MT}$ introduced in [10]. $\mathcal{MT}$-formulas are built from set variablesp1,p2,... (for arbitrary subsets of a metric space) using the Booleans ∧, ∨, →, and $\neg$, the distance operators$\exists^{ 0}$, and the topological interior and closure operatorsI and C. Intended models for this logic are of the form $\mathfrak I=(\Delta,d,p_{1}^{\mathfrak I},p_{2}^{\mathfrak I},\dots)$ where (Δ,d) is a metric space and $p_{i}^{\mathfrak I} \subseteq \Delta$. The extension$\varphi^{\mathfrak I} \subseteq \Delta$ of an $\mathcal{MT}$-formula ϕ in $\mathfrak I$ is defined inductively in the usual way, with I and C being interpreted as the interior and closure operators induced by the metric, and $(\exists^{

Propositional satisfiability (SAT) is one of the most important and central problems in Artificial Intelligence and Computer Science. Basically, most SAT solvers are based on the well-known Davis-Logemann-Loveland (DLL) procedure. DLL is a decision procedure: given a SAT formula φ, it can decide if φ is satisfiable (and it can return a satisfying assignment μ), or not. Often, this is not suffi- cient, in that we would like μ to be also "optimal", i.e., that has also to minimize/ maximize a given objective function. max-sat, min-one, distance-sat and their weighted versions are popular optimization problems. (In the following, φ is the input formula expressed as a set of clauses). Almost all the systems that can deal with these problems follow a classical branch&bound schema: whenever a satisfying assignment μ for φ with a cost cμ is found, the search goes on looking for another satisfying assignment with a lower (or higher, depending on the problem) cost. [ABSTRACT FROM AUTHOR]

Inductive Logic Programming (ILP) is a Machine Learning research field that has been quite successful in knowledge discovery in relational domains. ILP systems use a set of pre-classified examples (positive and negative) and prior knowledge to learn a theory in which positive examples succeed and the negative examples fail. In this paper we present a novel ILP system called April, capable of exploring several parallel strategies in distributed and shared memory machines. [ABSTRACT FROM AUTHOR]

Answer-set programming (ASP) has emerged as an important paradigm for declarative problem solving, and provides a host for many different application domains on the basis of nonmonotonic logic programs. The increasing popularity in ASP has raised also the interest in semantic comparisons of programs in ASP [3, 4], which are nowadays recognized as a theoretical basis for program optimization, where equivalencepreserving modifications are of primary interest; in particular, rewriting rules which allow to perform a local change in a program are important. Many such rules have been considered in the propositional setting (cf., e.g., [1, 6]) but just recently have been extended to the practicably important case of non-ground programs [2]. [ABSTRACT FROM AUTHOR]

Action languages [1] are a formal tool for reasoning about actions, where an agent's knowledge about a domain in question is represented by a declarative action description that consists of logical formulas. [ABSTRACT FROM AUTHOR]

Argumentation is becoming increasingly important in the design and implementation of autonomous software agents. In this paper we discuss our current work on a prototype lightweight Java-based argumentation engine that can be used to implement a non-monotonic reasoning component in Internet or agent-based applications. As far as possible we are aiming towards implementing a general purpose argumentation engine that can be configured to conform to one of a range of semantics. [ABSTRACT FROM AUTHOR]

In this paper we present a prototype of a tool that demonstrates how existing limitations in ensuring an agent's compliance to an argumentation-based dialogue protocol can be overcome. We also present the implementation of compliance enforcement components for a deliberation dialogue protocol, and an application that enables two human participants to engage in an efficiently moderated dialogue, where all inappropriate utterances attempted by an agent are blocked and prevented from inclusion within the dialogue. [ABSTRACT FROM AUTHOR]

We study causal information about probabilistic processes, i.e., information about why events occur. A language is developed in which such information can be formally represented and we investigate when this suffices to uniquely characterize the probability distribution that results from such a process. We examine both detailed representations of temporal aspects and representations in which time is implicit. In this last case, our logic turns into a more fine-grained version of Pearl's approach to causality. We relate our logic to certain probabilistic logic programming languages, which leads to a clearer view on the knowledge representation properties of these language. We show that our logic induces a semantics for disjunctive logic programs, in which these represent non-deterministic processes. We show that logic programs under the well-founded semantics can be seen as a language of deterministic causality, which we relate to McCain & Turner's causal theories. [ABSTRACT FROM AUTHOR]

We address the problem of evaluating ranked top-k queries in description logics. The problem occurs whenever we allow queries such as "find cheap hotels close to the conference location" in which fuzzy predicates like cheap and close occur. We show how to efficiently compute the top-k answers of conjunctive queries with fuzzy predicates over DL-LITE like knowledge bases. [ABSTRACT FROM AUTHOR]

The second postulate of Katsuno and Mendelzon characterizes irrelevant updates. We show that the postulate has to be modified, if nonmonotonic assumptions are considered. Our characterization of irrelevant updates is based on a dependency framework, which provides an alternative semantics of multidimensional dynamic logic programming. Keywords: foundations of logic-based AI systems, nonmonotonic knowledge bases, updates, logic programming, nonmonotonic reasoning. [ABSTRACT FROM AUTHOR]

This paper contributes to the identification, formalisation and analysis of desirable properties of agent models in general and of the KGP model in particular. This model is specified in computational logic, and consequently lends itself well to formal analysis. We formalise three notions of welfare, in terms of goal achievement, progress, and reactive awareness, and we prove results related to these notions for KGP agents. These results broadly demonstrate the coherence of some of the design decisions in the KGP model, the need for some of its components for effectiveness in goal achievement, the extent to which the welfare of KGP agents can be shown to improve during their life-time, and the awareness of the agents of their reactions to changes in the environment. [ABSTRACT FROM AUTHOR]

Although negative conclusions are presented implicitly in Normal Hybrid Probabilistic Programs (NHPP) [26] through the closed world assumption, representing and reasoning with explicit negation is needed in NHPP to allow the ability to reason with incomplete knowledge. In this paper we extend the language of NHPP to explicitly encode classical negation in addition to non-monotonic negation. The semantics of the extended language is based on the answer set semantics of traditional logic programming [9]. We show that the proposed semantics is a natural extension to the answer set semantics of traditional logic programming [9]. In addition, the proposed semantics is reduced to stable probabilistic model semantics of NHPP [26]. The importance of that is computational methods developed for NHPP can be applied to the proposed language. Furthermore, we show that some commonsense probabilistic knowledge can be easily represented in the proposed language. [ABSTRACT FROM AUTHOR]

Ontology evolution is an important problem in the Semantic Web research. Recently, Alchourrón, Gärdenfors and Markinson's (AGM) theory on belief change has been applied to deal with this problem. However, most of current work only focuses on the feasibility of the application of AGM postulates on contraction to description logics (DLs), a family of ontology languages. So the explicit construction of a revision operator is ignored. In this paper, we first generalize the AGM postulates on revision to DLs. We then define two revision operators in DLs. One is the weakening-based revision operator which is defined by weakening of statements in a DL knowledge base and the other is its refinement. We show that both operators capture some notions of minimal change and satisfy the generalized AGM postulates for revision. [ABSTRACT FROM AUTHOR]

In this paper, we extend on work presented in [1] where we proposed a method for reconstructing an agent's initial epistemic state from an observation on its belief revision behaviour. There, we assumed that the observation is complete in the sense that all revision inputs during the time of observation were known to us. Here, we drop this assumption and investigate the case where there are intermediate inputs we have no information about. The focus will be on determining the core belief of the agent — a belief the agent commits to at all times. [ABSTRACT FROM AUTHOR]

In this paper we show how the concepts of answer set programming and fuzzy logic can be succesfully combined into the single framework of fuzzy answer set programming (FASP). The framework offers the best of both worlds: from the answer set semantics, it inherits the truly declarative non-monotonic reasoning capabilities while, on the other hand, the notions from fuzzy logic in the framework allow it to step away from the sharp principles used in classical logic, e.g., that something is either completely true or completely false. As fuzzy logic gives the user great flexibility regarding the choice for the interpretation of the notions of negation, conjunction, disjunction and implication, the FASP framework is highly configurable and can, e.g., be tailored to any specific area of application. Finally, the presented framework turns out to be a proper extension of classical answer set programming, as we show, in contrast to other proposals in the literature, that there are only minor restrictions one has to demand on the fuzzy operations used, in order to be able to retrieve the classical semantics using FASP. [ABSTRACT FROM AUTHOR]

We study the deterministic Horn fragment of $\mathcal{ALC}$, which restricts the general Horn fragment of $\mathcal{ALC}$ only in that, the constructor ∀R.C is allowed in bodies of program clauses and queries only in the form $\forall\exists R.C$, which is defined as $\forall R.C \sqcap \exists R.C$. We present an algorithm that for a deterministic positive logic program P given as a TBox constructs a finite least pseudo-model $\mathcal{I}$ of P such that for every deterministic positive concept C, P ⊧C iff $\mathcal{I}$ validates C (and more strongly, iff $\mathcal{I},\tau \models C$, where τ is the distinguished object of $\mathcal{I}$ and the satisfaction means τ is an instance of C w.r.t. $\mathcal{I}$). Pseudo-interpretations are very similar to (traditional) interpretations, except that they have two interpretation functions for roles, one to deal with the constructor $\exists R.C$ and the other to deal with ∀R.C. They are ordered by comparing the sets of validated positive concepts. Our algorithm runs in time 2O(n) and returns a pseudo-interpretation of size 2O(n). Our method is extendable for instance checking w.r.t. knowledge bases containing also an ABox in more expressive description logics. [ABSTRACT FROM AUTHOR]

Efficient proof methods for normal modal logics are highly desirable, as such logical systems have been widely used in computer science to represent complex situations. Resolution-based methods are often designed to deal with formulae in a normal form and the efficiency of the method (also) relies on how efficient (in the sense of producing fewer and/or shorter clauses) the translation procedure is. We present a normal form for normal modal logics and show how the use of simplification, for specific normal logics, together with anti-prenexing and prenexing techniques help us to produce better sets of clauses. [ABSTRACT FROM AUTHOR]

In this paper we motivate and formalise a framework that organises Dung argumentation frameworks into a hierarchy. Argumentation over preference information in a level n Dung framework is then used to resolve conflicts between arguments in a level n-1 framework. We then re-examine the issue of Dung's acceptability semantics for arguments from the perspective of hierarchical argumentation. [ABSTRACT FROM AUTHOR]

The most recent version of defeasible logic (Nute, 1997) is related to the well-founded semantics by translating defeasible theories into normal logic programs using a simple scheme proposed in (Brewka, 2001). It is found that by introducing ambiguity propagation into this logic, the assertions of defeasible theories coincide with the well-founded models of their logic program translations. Without this addition, the two formalisms are found to disagree in important cases. A translation in the other direction is also provided. By treating default negated atoms as presumptions in defeasible logic, normal logic programs can be converted into equivalent defeasible theories. [ABSTRACT FROM AUTHOR]

In this paper we reduce the question of validity of a first-order intuitionistic formula without equality to generating ground instances of this formula and then checking whether the instances are deducible in a propositional intuitionistic tableaux calculus, provided that the propositional proof is compatible with the way how the instances were generated. This result can be seen as a form of the Herbrand theorem, and so it provides grounds for further theoretical investigation of computer-oriented intuitionistic calculi. [ABSTRACT FROM AUTHOR]

The main objective of this work is to develop a multi-modal logic of Intention and Attempt. We call this logic LIA. All formal results are focused on the notion of attempt. We substitute the dynamic molecular notion action by his atomic constituent attempt and define the former from the latter. The relations between attempts, goals, beliefs and present-directed intentions are studied. A section of the paper is devoted to the analysis of the relations of our modal logic with a situation calculus-style approach. [ABSTRACT FROM AUTHOR]

Action formalisms based on description logics (DLs) have recently been introduced as decidable fragments of well-established action theories such as the Situation Calculus and the Fluent Calculus. However, existing DL action formalisms fail to include general TBoxes, which are the standard tool for formalising ontologies in modern description logics. We define a DL action formalism that admits general TBoxes, propose an approach to addressing the ramification problem that is introduced in this way, show that our formalism is decidable and perform a detailed investigation of its computational complexity. [ABSTRACT FROM AUTHOR]

Reiter's default logic can not handle inconsistencies and incoherences and thus is not satisfactory enough in commonsense reasoning. In the paper we propose a new variant of default logic named FDL in which the existence of extension is guaranteed and the trivial extension is avoided. Moreover, Reiter's default extensions are reserved and can be identified from the other extensions in FDL. Technically, we develop a paraconsistent and monotonic reasoning system based on resolution as the underlying logic of FDL. The definition of extension is also modified in the manner that conflicts between justifications of the used defaults and the conclusions of the extension, which we call justification conflicts, are permitted, so that justifications can not be denied by "subsequent" defaults and the existence of extension is guaranteed. Then we select the desired extensions as preferred ones according to the criteria that justification conflicts should be minimal. [ABSTRACT FROM AUTHOR]

The work deals with deductive synthesis of functional programs. During this synthesis formal specification of a program is taken as a mathe-matical existence theorem and while proving it, we derive a program and prove that this program corresponds to given specification. Our method of synthesis is based on the deductive tableau method, that allows to derive three basic constructions of a functional program. But the full search of possible proof attempts in the deductive tableau induces a very large search space; the proof is needed to be guided. For using this method in the automatic mode additional heuristics are required. Some of such heuristics are proposed in this work. They consist in proof planning by using rippling and in the use of sorted logic with type hierarchy that reduces search space and blocks some branches of proof, corresponding to synthesis of incorrect functions. The proposed techniques are implemented in the system ALISAALISA - Automatic LIsp Synthesizer. and used for automatic synthesis of several functions on Lisp language. [ABSTRACT FROM AUTHOR]