Characterizations of semi-stable and stage extensions in terms of two-valued logical models are presented. To this end, the so-called GL-supported and GL-stage models are defined. These two classes of logical models a...
详细信息
Characterizations of semi-stable and stage extensions in terms of two-valued logical models are presented. To this end, the so-called GL-supported and GL-stage models are defined. These two classes of logical models are logicprogramming counterparts of the notion of range which is an established concept in argumentation semantics.
Oz is a multiparadigm language that supports logicprogramming as one of its major paradigms. A multiparadigm language is designed to support different programming paradigms (logic, functional, constraint, object-orie...
详细信息
Oz is a multiparadigm language that supports logicprogramming as one of its major paradigms. A multiparadigm language is designed to support different programming paradigms (logic, functional, constraint, object-oriented, sequential, concurrent, etc.) with equal ease. This paper has two goals: to give a tutorial of logicprogramming in Oz;and to show how logicprogramming fits naturally into the wider context of multiparadigm programming. Our experience shows that there are two classes of problems, which we call algorithmic and search problems, for which logicprogramming can help formulate practical solutions. Algorithmic problems have known efficient algorithms. Search problems do not have known efficient algorithms but can be solved with search. The Oz support for logicprogramming targets these two problem classes specifically, using the concepts needed for each. This is in contrast to the Prolog approach, which targets both classes with one set of concepts, which results in less than optimal support for each class. We give examples that can be run interactively on the Mozart system, which implements Oz, To explain the essential difference between algorithmic and search programs, we define the Oz execution model. This model subsumes both concurrent logicprogramming (committed-choice-style) and search-based logicprogramming (Prolog-style). Furthermore, as consequences of its multiparadigm nature, the model supports new abilities such as first-class top levels, deep guards, active objects, and sophisticated control of the search process. Instead of Horn clause syntax, Oz has a simple, fully compositional, higher-order syntax that accommodates the abilities of the language. We give a brief history of Oz that traces the development of its main ideas and we summarize the lessons learned from this work. Finally, we give many entry points into the Oz literature.
Tabled Constraint logicprogramming is a powerful execution mechanism for dealing with Constraint logicprogramming without worrying about fixpoint computation. Various applications, e.g. in the fields of program anal...
详细信息
Tabled Constraint logicprogramming is a powerful execution mechanism for dealing with Constraint logicprogramming without worrying about fixpoint computation. Various applications, e.g. in the fields of program analysis and model checking, have been proposed. Unfortunately, a high-level system for developing new applications is lacking, and programmers are forced to resort to complicated ad hoc solutions. This papers presents TCHR, a high-level framework for tabled Constraint logicprogramming. It integrates in a light-weight manner Constraint Handling Rules (CHR), a high-level language for constraint solvers, with tabled logicprogramming. The framework is easily instantiated with new application-specific constraint domains. Various high-level operations can be instantiated to control performance. In particular, we propose a novel, generalized technique for compacting answer sets.
The supertree construction problem is about combining several phylogenetic trees with possibly conflicting information into a single tree that has all the leaves of the source trees as its leaves and the relationships...
详细信息
The supertree construction problem is about combining several phylogenetic trees with possibly conflicting information into a single tree that has all the leaves of the source trees as its leaves and the relationships between the leaves are as consistent with the source trees as possible. This leads to an optimization problem that is computationally challenging and typically heuristic methods, such as matrix representation with parsimony (MRP), are used. In this paper we consider the use of answer set programming to solve the supertree construction problem in terms of two alternative encodings. The first is based on an existing encoding of trees using substructures known as quartets, while the other novel encoding captures the relationships present in trees through direct projections. We use these encodings to compute a genus-level supertree for the family of cats (Felidae). Furthermore, we compare our results to recent supertrees obtained by the MRP method.
Epistemic logic Programs (ELPs) extend Answer Set programming (ASP) with epistemic negation and have received renewed interest in recent years. This led to the development of new research and efficient solving systems...
详细信息
Epistemic logic Programs (ELPs) extend Answer Set programming (ASP) with epistemic negation and have received renewed interest in recent years. This led to the development of new research and efficient solving systems for ELPs. In practice, ELPs are often written in a modular way, where each module interacts with other modules by accepting sets of facts as input, and passing on sets of facts as output. An interesting question then presents itself: under which conditions can such a module be replaced by another one without changing the outcome, for any set of input facts? This problem is known as uniform equivalence, and has been studied extensively for ASP. For ELPs, however, such an investigation is, as of yet, missing. In this paper, we therefore propose a characterization of uniform equivalence that can be directly applied to the language of state-of-the-art ELP solvers. We also investigate the computational complexity of deciding uniform equivalence for two ELPs, and show that it is on the third level of the polynomial hierarchy.
In this paper we compare three different formalisms that can be used in the area of models for distributed, concurrent and mobile systems. In particular we analyze the relationships between a process calculus, the Fus...
详细信息
In this paper we compare three different formalisms that can be used in the area of models for distributed, concurrent and mobile systems. In particular we analyze the relationships between a process calculus, the Fusion Calculus, graph transformations in the Synchronized Hyperedge Replacement with Hoare synchronization (HSHR) approach and logicprogramming. We present a translation from Fusion Calculus into HSHR (whereas Fusion Calculus uses Milner synchronization) and prove a correspondence between the reduction semantics of Fusion Calculus and HSHR transitions. We also present a mapping from HSHR into a transactional version of logicprogramming and prove that there is a full correspondence between the two formalisms. The resulting mapping from Fusion Calculus to logicprogramming is interesting since it shows the tight analogies between the two formalisms, in particular for handling name generation and mobility. The intermediate step in terms of HSHR is convenient since graph transformations allow for multiple, remote synchronizations, as required by Fusion Calculus semantics.
We provide a comprehensive elaboration of the theoretical foundations of variable instantiation, or grounding, in Answer Set programming (ASP). Building on the semantics of ASP's modeling language, we introduce a ...
详细信息
We provide a comprehensive elaboration of the theoretical foundations of variable instantiation, or grounding, in Answer Set programming (ASP). Building on the semantics of ASP's modeling language, we introduce a formal characterization of grounding algorithms in terms of (fixed point) operators. A major role is played by dedicated well-founded operators whose associated models provide semantic guidance for delineating the result of grounding along with on-the-fly simplifications. We address an expressive class of logic programs that incorporates recursive aggregates and thus amounts to the scope of existing ASP modeling languages. This is accompanied with a plain algorithmic framework detailing the grounding of recursive aggregates. The given algorithms correspond essentially to the ones used in the ASP grounder gringo.
Many real world domains require the representation of a measure of uncertainty. The most common such representation is probability, and the combination of probability with logic programs has given rise to the field of...
详细信息
Many real world domains require the representation of a measure of uncertainty. The most common such representation is probability, and the combination of probability with logic programs has given rise to the field of Probabilistic logicprogramming (PLP), leading to languages such as the Independent Choice logic, logic Programs with Annotated Disjunctions (LPADs), Problog, PRISM, and others. These languages share a similar distribution semantics, and methods have been devised to translate programs between these languages. The complexity of computing the probability of queries to these general PLP programs is very high due to the need to combine the probabilities of explanations that may not be exclusive. As one alternative, the PRISM system reduces the complexity of query answering by restricting the form of programs it can evaluate. As an entirely different alternative, Possibilistic logic Programs adopt a simpler metric of uncertainty than probability. Each of these approaches-general PLP, restricted PLP, and Possibilistic logicprogramming-can be useful in different domains depending on the form of uncertainty to be represented, on the form of programs needed to model problems, and on the scale of the problems to be solved. In this paper, we show how the PITA system, which originally supported the general PLP language of LPADs, can also efficiently support restricted PLP and Possibilistic logic Programs. PITA relies on tabling with answer subsumption and consists of a transformation along with an API for library functions that interface with answer subsumption. We show that, by adapting its transformation and library functions, PITA can be parameterized to PITA(IND,EXC) which supports the restricted PLP of PRISM, including optimizations that reduce non-discriminating arguments and the computation of Viterbi paths. Furthermore, we show PITA to be competitive with PRISM for complex queries to Hidden Markov Model examples, and sometimes much faster. We further show
Distribution semantics is one of the most prominent approaches for the combination of logicprogramming and probability theory. Many languages follow this semantics, such as Independent Choice logic, PRISM, pD, logic ...
详细信息
Distribution semantics is one of the most prominent approaches for the combination of logicprogramming and probability theory. Many languages follow this semantics, such as Independent Choice logic, PRISM, pD, logic Programs with Annotated Disjunctions (LPADs), and ProbLog. When a program contains functions symbols, the distribution semantics is well-defined only if the set of explanations for a query is finite and so is each explanation. Well-definedness is usually either explicitly imposed or is achieved by severely limiting the class of allowed programs. In this paper, we identify a larger class of programs for which the semantics is well-defined together with an efficient procedure for computing the probability of queries. Since logic Programs with Annotated Disjunctions offer the most general syntax, we present our results for them, but our results are applicable to all languages under the distribution semantics. We present the algorithm "Probabilistic Inference with Tabling and Answer subsumption" (PITA) that computes the probability of queries by transforming a probabilistic program into a normal program and then applying SLG resolution with answer subsumption. PITA has been implemented in XSB and tested on six domains: two with function symbols and four without. The execution times are compared with those of ProbLog, cplint, and CVE. PITA was almost always able to solve larger problems in a shorter time, on domains with and without function symbols.
The paper introduces FUZZY linguistic logicprogramming, which is a combination of fuzzy logicprogramming, introduced by P. Vojtas, and hedge algebras in order to facilitate the representation and reasoning on human ...
详细信息
The paper introduces FUZZY linguistic logicprogramming, which is a combination of fuzzy logicprogramming, introduced by P. Vojtas, and hedge algebras in order to facilitate the representation and reasoning on human knowledge expressed in natural languages. In fuzzy linguistic logicprogramming, truth values are linguistic ones, e.g., Very True, Very Probably True and Little False, taken from a hedge algebra of a linguistic truth variable, and linguistic hedges (modifiers) can be used as unary connectives in formulae. This is motivated by the fact that humans reason mostly in terms of linguistic terms rather than in terms of numbers, and linguistic hedges are often used in natural languages to express different levels of emphasis. The paper presents: (a) the language Of fuzzy linguistic logicprogramming;(b) a declarative semantics in terms of Herbrand interpretations and models;(c) a procedural semantics which directly manipulates linguistic terms to Compute a lower bound to the truth Value of a query, and proves its soundness;(d) a fixpoint semantics of logic programs, and based on it, proves the completeness of the procedural semantics;(e) several applications of fuzzy linguistic logicprogramming;and (f) an idea of implementing a system to execute fuzzy linguistic logic programs.
暂无评论