Extensional higher-order logicprogramming has been introduced as a generalization of classical logicprogramming. An important characteristic of this paradigm is that it preserves all the well-known properties of tra...
详细信息
Extensional higher-order logicprogramming has been introduced as a generalization of classical logicprogramming. An important characteristic of this paradigm is that it preserves all the well-known properties of traditional logicprogramming. In this paper we consider the semantics of negation in the context of the new paradigm. Using some recent results from non-monotonic fixed-point theory, we demonstrate that every higher-order logic program with negation has a unique minimum infinite-valued model. In this way we obtain the first purely model-theoretic semantics for negation in extensional higher-order logicprogramming. Using our approach, we resolve an old paradox that was introduced by W. W. Wadge in order to demonstrate the semantic difficulties of higher-order logicprogramming.
Modern functional logicprogramming (FLP) languages use non-terminating and non-confluent constructor systems (CSs) as programs in order to define non-strict and non-deterministic functions. Two semantic alternatives ...
详细信息
Modern functional logicprogramming (FLP) languages use non-terminating and non-confluent constructor systems (CSs) as programs in order to define non-strict and non-deterministic functions. Two semantic alternatives have been usually considered for parameter passing with this kind of functions: call-time choice and run-time choice. While the former is the standard choice of modern FLP languages, the latter lacks some basic properties - mainly compositionality - that have prevented its use in practical FLP systems. Traditionally it has been considered that call-time choice induces a singular denotational semantics, while run-time choice induces a plural semantics. We have discovered that this latter identification is wrong when pattern matching is involved, and thus in this paper we propose two novel compositional plural semantics for CSs that are different from run-time choice. We investigate the basic properties of our plural semantics - compositionality, polarity, and monotonicity for substitutions, and a restricted form of the bubbling property for CSs - and the relation between them and to previous proposals, concluding that these semantics form a hierarchy in the sense of set inclusion of the set of values computed by them. Besides, we have identified a class of programs characterized by a simple syntactic criterion for which the proposed plural semantics behave the same, and a program transformation that can be used to simulate one of the proposed plural semantics by term rewriting. At the practical level, we study how to use the new expressive capabilities of these semantics for improving the declarative flavor of programs. As call-time choice is the standard semantics for FLP, it still remains the best option for many common programming patterns. Therefore, we propose a language that combines call-time choice and our plural semantics, which we have implemented in the Maude system. The resulting interpreter is then employed to develop and test several signif
The paper presents a knowledge representation language Alog which extends ASP with aggregates. The goal is to have a language based on simple syntax and clear intuitive and mathematical semantics. We give some propert...
详细信息
The paper presents a knowledge representation language Alog which extends ASP with aggregates. The goal is to have a language based on simple syntax and clear intuitive and mathematical semantics. We give some properties of Alog, an algorithm for computing its answer sets, and comparison with other approaches.
Describing complex objects by elementary ones is a common strategy in mathematics and science in general. In their seminal 1965 paper, Kenneth Krohn and John Rhodes showed that every finite deterministic automaton can...
详细信息
Describing complex objects by elementary ones is a common strategy in mathematics and science in general. In their seminal 1965 paper, Kenneth Krohn and John Rhodes showed that every finite deterministic automaton can be represented (or "emulated") by a cascade product of very simple automata. This led to an elegant algebraic theory of automata based on finite semigroups (Krohn-Rhodes theory). Surprisingly, by relating logic programs and automata, we can show in this paper that the Krohn-Rhodes theory is applicable in Answer Set programming (ASP). More precisely, we recast the concept of a cascade product to ASP, and prove that every program can be represented by a product of very simple programs, the reset and standard programs. Roughly, this implies that the reset and standard programs are the basic building blocks of ASP with respect to the cascade product. In a broader sense, this paper is a first step towards an algebraic theory of products and networks of nonmonotonic reasoning systems based on Krohn-Rhodes theory, aiming at important open issues in ASP and AI in general.
In answer set programming, inconsistencies arise when the constraints placed on a program become unsatisfiable. In this paper, we introduce a technique for dynamic consistency checking for our goal-directed method for...
详细信息
In answer set programming, inconsistencies arise when the constraints placed on a program become unsatisfiable. In this paper, we introduce a technique for dynamic consistency checking for our goal-directed method for computing answer sets, under which only those constraints deemed relevant to the partial answer set are tested, allowing inconsistent knowledgebases to be successfully queried. However, the algorithm guarantees that, if a program has at least one consistent answer set, any partial answer set returned will be a subset of some consistent answer set.
In this work we propose a multi-valued extension of logic programs under the stable models semantics where each true atom in a model is associated with a set of justifications. These justifications are expressed in te...
详细信息
In this work we propose a multi-valued extension of logic programs under the stable models semantics where each true atom in a model is associated with a set of justifications. These justifications are expressed in terms of causal graphs formed by rule labels and edges that represent their application ordering. For positive programs, we show that the causal justifications obtained for a given atom have a direct correspondence to (relevant) syntactic proofs of that atom using the program rules involved in the graphs. The most interesting contribution is that this causal information is obtained in a purely semantic way, by algebraic operations (product, sum and application) on a lattice of causal values whose ordering relation expresses when a justification is stronger than another. Finally, for programs with negation, we define the concept of causal stable model by introducing an analogous transformation to Gelfond and Lifschitz's program reduct. As a result, default negation behaves as "absence of proof" and no justification is derived from negative literals, something that turns out convenient for elaboration tolerance, as we explain with a running example.
This paper investigates specifying and solving linear time-dependent constraints with an interval temporal logicprogramming language MSVL. To this end, linear constraint statements involving linear equality and non-s...
详细信息
This paper investigates specifying and solving linear time-dependent constraints with an interval temporal logicprogramming language MSVL. To this end, linear constraint statements involving linear equality and non-strict inequality are first defined. Further, the time-dependent relations in the constraints are specified by temporal operators, such as . Thus, linear time-dependent constraints can be smoothly incorporated into MSVL. Moreover, to solve the linear constraints within MSVL by means of reduction, the operational semantics for linear constraints is given. In particular, semantic equivalence rules and transition rules within a state are presented, which enable us to reduce linear equations, inequalities and optimization problems in a convenient way. Besides, the operational semantics is proved to be sound. Finally, a production scheduling application is provided to illustrate how our approach works in practice.
We have designed a new logicprogramming language called LM (Linear Meld) for programming graph- based algorithms in a declarative fashion. Our language is based on linear logic, an expressive logical system where log...
详细信息
We have designed a new logicprogramming language called LM (Linear Meld) for programming graph- based algorithms in a declarative fashion. Our language is based on linear logic, an expressive logical system where logical facts can be consumed. Because LM integrates both classical and linear logic, LM tends to be more expressive than other logicprogramming languages. LM programs are naturally concurrent because facts are partitioned by nodes of a graph data structure. Computation is performed at the node level while communication happens between connected nodes. In this paper, we present the syntax and operational semantics of our language and illustrate its use through a number of examples.
Concurrent Constraint programming (CCP) is a simple and powerful model for concurrency where agents interact by telling and asking constraints. Since their inception, CCP-languages have been designed for having a stro...
详细信息
Concurrent Constraint programming (CCP) is a simple and powerful model for concurrency where agents interact by telling and asking constraints. Since their inception, CCP-languages have been designed for having a strong connection to logic. In fact, the underlying constraint system can be built from a suitable fragment of intuitionistic (linear) logic -ILL- and processes can be interpreted as formulas in ILL. Constraints as ILL formulas fail to represent accurately situations where "preferences" (called soft constraints) such as probabilities, uncertainty or fuzziness are present. In order to circumvent this problem, c-semirings have been proposed as algebraic structures for defining constraint systems where agents are allowed to tell and ask soft constraints. Nevertheless, in this case, the tight connection to logic and proof theory is lost. In this work, we give a proof theoretical meaning to soft constraints: they can be defined as formulas in a suitable fragment of ILL with subexponentials (SELL) where subexponentials, ordered in a c-semiring structure, are interpreted as preferences. We hence achieve two goals: (1) obtain a CCP language where agents can tell and ask soft constraints and (2) prove that the language in (1) has a strong connection with logic. Hence we keep a declarative reading of processes as formulas while providing a logical framework for soft-CCP based systems. An interesting side effect of (1) is that one is also able to handle probabilities (and other modalities) in SELL, by restricting the use of the promotion rule for non-idempotent c-semirings. This finer way of controlling subexponentials allows for considering more interesting spaces and restrictions, and it opens the possibility of specifying more challenging computational systems.
When developing a (web) interface for a deductive database, functionality required by the client is provided by means of HTTP handlers that wrap the logical data access predicates. These handlers are responsible for c...
详细信息
When developing a (web) interface for a deductive database, functionality required by the client is provided by means of HTTP handlers that wrap the logical data access predicates. These handlers are responsible for converting between client and server data representations and typically include options for paginating results. Designing the web accessible API is difficult because it is hard to predict the exact requirements of clients. Pengines changes this picture. The client provides a Prolog program that selects the required data by accessing the logical API of the server. The pengine infrastructure provides general mechanisms for converting Prolog data and handling Prolog non-determinism. The Pengines library is small (2000 lines Prolog, 150 lines JavaScript). It greatly simplifies defining an AJAX based client for a Prolog program and provides non-deterministic RPC between Prolog processes as well as interaction with Prolog engines similar to Paul Tarau's engines. Pengines are available as a standard package for SWI-Prolog 7.(1)
暂无评论