We consider disjunctive logic programs without function symbols but with existential quantification in rule heads, under the semantics of general stable models. There are at least two interesting prospects in these pr...
详细信息
We consider disjunctive logic programs without function symbols but with existential quantification in rule heads, under the semantics of general stable models. There are at least two interesting prospects in these programs. The first is that a program can be made more succinct by using existential variables, and the second is on the potential in representing defeasible ontological knowledge by these logic programs. This paper studies some of the properties of these programs. First, we show a simple yet intuitive definition of stable models for these programs that does not resort to second-order logic. Second, the stable models of these programs can be characterized by an extension of progression for disjunctive programs, which provides a native characterization of justification for stable models. We then study the decidability issue. While the stable model existence problem for safe disjunctive programs is decidable, with existential quantification allowed in rule heads the problem becomes undecidable. We identify an interesting decidable fragment by exploring a new notion of stratification over existential quantification.
The paper presents a knowledge representation formalism, in the form of a high-level Action Description Language (ADL) for multi-agent systems, where autonomous agents reason and act in a shared environment. Agents ar...
详细信息
The paper presents a knowledge representation formalism, in the form of a high-level Action Description Language (ADL) for multi-agent systems, where autonomous agents reason and act in a shared environment. Agents are autonomously pursuing individual goals, but are capable of interacting through a shared knowledge repository. In their interactions through shared portions of the world, the agents deal with problems of synchronization and concurrency;the action language allows the description of strategies to ensure a consistent global execution of the agents' autonomously derived plans. A distributed planning problem is formalized by providing the declarative specifications of the portion of the problem pertaining to a single agent. Each of these specifications is executable by a stand-alone CLP-based planner. The coordination among agents exploits a Linda infrastructure. The proposal is validated in a prototype implementation developed in SICStus Prolog.
A large body of work has been dedicated to termination analysis of logic programs but relatively little has been done to analyze non-termination. In our opinion, explaining non-termination is a much more important tas...
详细信息
A large body of work has been dedicated to termination analysis of logic programs but relatively little has been done to analyze non-termination. In our opinion, explaining non-termination is a much more important task because it can dramatically improve a user's ability to effectively debug large, complex logic programs without having to abide by punishing syntactic restrictions. Non-termination analysis examines program execution history when the program is suspected to not terminate and informs the programmer about the exact reasons for this behavior. In Liang and Kifer (2013), we studied the problem of non-termination in tabled logic engines with subgoal abstraction, such as XSB, and proposed a suite of algorithms for non-termination analysis, called Terminyzer. These algorithms analyze forest logging traces and output sequences of tabled subgoal calls that are the likely causes of non-terminating cycles. However, this feedback was hard to use in practice: the same subgoal could occur in multiple rule heads and in even more places in rule bodies, so Terminyzer left too much tedious, sometimes combinatorially large amount of work for the user to do manually. Here we propose a new suite of algorithms, Terminyzer(+), which closes this usability gap. Terminyzer+ can detect not only sequences of subgoals that cause non-termination, but, importantly, the exact rules where they occur and the rule sequences that get fired in a cyclic manner, thus causing non-termination. This makes Terminyzer(+) suitable as a back-end for user-friendly graphical interfaces on top of Terminyzer(+), which can greatly simplify the debugging process. Terminyzer(+) back-ends exist for the SILK system as well as for the open-source Flora-2 system. A graphical interface has been developed for SILK and is currently underway for Flora-2. We also report experimental studies, which confirm the effectiveness of Terminyzer(+) on a host of large real-world knowledge bases. All tests used in this pape
Answer Set programming (ASP) is a powerful form of declarative programming used in areas such as planning or reasoning. ASP solvers enforce stable model semantics, which rule out solutions representing certain kinds o...
详细信息
Answer Set programming (ASP) is a powerful form of declarative programming used in areas such as planning or reasoning. ASP solvers enforce stable model semantics, which rule out solutions representing certain kinds of circular reasoning. Unfortunately, current ASP solvers are incapable of solving problems involving cyclic dependencies between multiple integer or continuous quantities effectively. In this paper, we generalize the notion of stable models to bound founded variables with arbitrary domains, where bounds on such variables need to be justified by some rule in the program in order for the model to be stable. We show how to handle significantly more general rule forms where bound founded variables can act as head or body variables, and where head and body variables can be related via complex constraints subject to certain monotonicity requirements. We describe a new unfounded set detection algorithm which allows us to enforce this generalization of the stable model semantics. We also show how these unfounded sets can be explained in order to allow effective conflict-directed clause learning. The new solver merges the best features of CP, SAT and ASP solvers and allows new types of problems to be solved very efficiently.
The widespread availability of large data-sets poses both an opportunity and a challenge to logicprogramming. A first approach is to couple a relational database with logicprogramming, say, a Prolog system with MySQ...
详细信息
The widespread availability of large data-sets poses both an opportunity and a challenge to logicprogramming. A first approach is to couple a relational database with logicprogramming, say, a Prolog system with MySQL. While this approach does pay off in cases where the data cannot reside in main memory, it is known to introduce substantial overheads. Ideally, we would like the Prolog system to deal with large data-sets in an efficient way both in terms of memory and of processing time. Just In Time Indexing (JITI) was mainly motivated by this challenge, and can work quite well in many application. Exo-compilation, designed to deal with large tables, is a next step that achieves very interesting results, reducing the memory footprint over two thirds. We show that combining exo-compilation with Just In Time Indexing can have significant advantages both in terms of memory usage and in terms of execution time. An alternative path that is relevant for many applications is User-Defined Indexing (UDI). This allows the use of specialized indexing for specific applications, say the spatial indexing crucial to any spatial system. The UDI sees indexing as pluggable modules, and can naturally be combined with Exo-compilation. We do so by using UDI with exo-data, and incorporating ideas from the UDI into high-performance indexers for specific tasks.
Increasingly huge amounts of data are published on the Web, and generated from sensors and social media. This Big Data challenge poses new scientific and technological challenges and creates new opportunities - thus t...
详细信息
Fuzzy Linear programming models are quite frequent in practice. The dynamic nature of the real problems often requires reoptimize from the optimal solutions found, what may mean a significant consumption of time and f...
详细信息
ISBN:
(纸本)9789078677789
Fuzzy Linear programming models are quite frequent in practice. The dynamic nature of the real problems often requires reoptimize from the optimal solutions found, what may mean a significant consumption of time and funds. In this paper, in order to efficiently solve this problem, first the optimality conditions and the duality results for fully fuzzy linear programming problems (all parameters and variables are symmetric trapezoidal fuzzy numbers) are generalized. Then, one proposes a fuzzy dual simplex method for solving these problems without the need of converting them to conventional linear programming problems. The resulting algorithm is flexible and easy of applying. For the sake of illustration, finally, an easy example is solved.
SAT Modulo Theories (SMT) is the problem of determining the satisfiability of a formula in which constraints, drawn from a given constraint theory T, are composed with logical connectives. The DPLL(T) approach to SMT ...
详细信息
Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, wh...
详细信息
Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself. We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's canonical structures, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logicprogramming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.
Rewriting logic is an executable logical framework well suited for the semantic definition of languages. Any such framework has to be judged by its effectiveness to bridge the existing gap between language definitions...
详细信息
ISBN:
(纸本)9783642229527
Rewriting logic is an executable logical framework well suited for the semantic definition of languages. Any such framework has to be judged by its effectiveness to bridge the existing gap between language definitions on the one hand, and language implementations and language analysis tools on the other. We give a progress report on how researchers in the rewriting logic semantics project are narrowing the gap between theory and practice in areas such as: modular semantic definitions of languages;scalability to real languages;support for real time;semantics of software and hardware modeling languages;and semantics-based analysis tools such as static analyzers, model checkers, and program provers. (C) 2013 Published by Elsevier Inc.
暂无评论