scholarly journals Decidability of the Clark's completion semantics for monadic programs and queries

2014 ◽  
Vol 15 (3) ◽  
pp. 402-412
Author(s):  
LEVON HAYKAZYAN
Keyword(s):  
Logic Programming ◽  
Logic Programs ◽  
First Order ◽  
Order Language ◽  
General Logic ◽  
Turing Complete

AbstractThere are many different semantics for general logic programs (i.e. programs that use negation in the bodies of clauses). Most of these semantics are Turing complete (in a sense that can be made precise), implying that they are undecidable. To obtain decidability one needs to put additional restrictions on programs and queries. In logic programming it is natural to put restrictions on the underlying first-order language. In this note, we show the decidability of the Clark's completion semantics for monadic general programs and queries.

Topological Model Set Deformations in Logic Programming

1989 ◽  
Vol 12 (3) ◽  
pp. 357-399
Author(s):  
Aida Batarekh ◽  
V.S. Subrahmanian
Keyword(s):  
Logic Programming ◽  
Sufficient Conditions ◽  
Topological Spaces ◽  
Logic Programs ◽  
First Order ◽  
Order Language ◽  
Language L ◽  
General Logic ◽  
Model Set ◽  
Necessary And Sufficient

Given a first order language L, and a notion of a logic L w.r.t. L, we investigate the topological properties of the space of L-structures for L. We show that under a topology called the query topology which arises naturally in logic programming, the space of L-models (where L is a decent logic) of any sentence (set of clauses) in L may be regarded as a (closed, compact) T4-space. We then investigate the properties of maps from structures to structures. Our results allow us to apply various well-known results on the fixed-points of operators on topological spaces to the semantics of logic programming – in particular, we are able to derive necessary and sufficient topological conditions for the completion of covered general logic programs to be consistent. Moreover, we derive sufficient conditions guaranteeing the consistency of program completions, and for logic programs to be determinate. We also apply our results to characterize consistency of the unions of program completions.

scholarly journals Productive corecursion in logic programming

2017 ◽  
Vol 17 (5-6) ◽  
pp. 906-923 ◽  
Author(s):  
EKATERINA KOMENDANTSKAYA ◽  
YUE LI
Keyword(s):  
Data Structure ◽  
Logic Programming ◽  
State Of The Art ◽  
Logic Program ◽  
Stream Processing ◽  
The Internet ◽  
Logic Programs ◽  
Algorithmic Solution ◽  
Undecidable Property ◽  
Turing Complete

AbstractLogic Programming is a Turing complete language. As a consequence, designing algorithms that decide termination and non-termination of programs or decide inductive/coinductive soundness of formulae is a challenging task. For example, the existing state-of-the-art algorithms can only semi-decide coinductive soundness of queries in logic programming for regular formulae. Another, less famous, but equally fundamental and important undecidable property is productivity. If a derivation is infinite and coinductively sound, we may ask whether the computed answer it determines actually computes an infinite formula. If it does, the infinite computation is productive. This intuition was first expressed under the name of computations at infinity in the 80s. In modern days of the Internet and stream processing, its importance lies in connection to infinite data structure processing. Recently, an algorithm was presented that semi-decides a weaker property – of productivity of logic programs. A logic program is productive if it can give rise to productive derivations. In this paper, we strengthen these recent results. We propose a method that semi-decides productivity of individual derivations for regular formulae. Thus, we at last give an algorithmic counterpart to the notion of productivity of derivations in logic programming. This is the first algorithmic solution to the problem since it was raised more than 30 years ago. We also present an implementation of this algorithm.

scholarly journals Composing programs in a rewriting logic for declarative programming

2003 ◽  
Vol 3 (2) ◽  
pp. 189-221 ◽  
Author(s):  
J. M. MOLINA-BRAVO ◽  
E. PIMENTEL
Keyword(s):  
Logic Programming ◽  
Declarative Programming ◽  
Rewriting Logic ◽  
Logic Programs ◽  
Alternative Semantics ◽  
Program Module ◽  
First Order ◽  
Natural Notion ◽  
Functional Logic ◽  
Simple Notion

Constructor-Based Conditional Rewriting Logic is a general framework for integrating first-order functional and logic programming which gives an algebraic semantics for nondeterministic functional-logic programs. In the context of this formalism, we introduce a simple notion of program module as an open program which can be extended together with several mechanisms to combine them. These mechanisms are based on a reduced set of operations. However, the high expressiveness of these operations enable us to model typical constructs for program modularization like hiding, export/import, genericity/instantiation, and inheritance in a simple way. We also deal with the semantic aspects of the proposal by introducing an immediate consequence operator, and studying several alternative semantics for a program module, based on this operator, in the line of logic programming: the operator itself, its least fixpoint (the least model of the module), the set of its pre-fixpoints (term models of the module), and some other variations in order to find a compositional and fully abstract semantics w.r.t. the set of operations and a natural notion of observability.

Protected completions of first-order general logic programs

1990 ◽  
Vol 6 (2) ◽  
pp. 147-172 ◽  
Author(s):  
James J. Lu ◽  
V. S. Subrahmanian
Keyword(s):  
Logic Programs ◽  
First Order ◽  
General Logic

scholarly journals First-Order Modular Logic Programs and their Conservative Extensions (Extended Abstract)

2017 ◽  
Author(s):  
Amelia Harrison ◽  
Yuliya Lierler
Keyword(s):  
Logic Programming ◽  
Short Version ◽  
Logic Programs ◽  
Conservative Extension ◽  
International Conference ◽  
First Order ◽  
Modular Logic ◽  
Traditional Programs ◽  
The Common ◽  
Conservative Extensions

This paper introduces first-order modular logic programs, which provide a way of viewing answer set programs as consisting of many independent, meaningful modules. We also present conservative extensions of such programs. This concept helps to identify strong relationships between modular programs as well as between traditional programs. For example, we illustrate how the notion of a conservative extension can be used to justify the common projection rewriting. This is a short version of a paper was presented at the 32nd International Conference on Logic Programming (Harrison and Lierler, 2016).

scholarly journals Representing first-order causal theories by logic programs

2011 ◽  
Vol 12 (3) ◽  
pp. 383-412 ◽  
Author(s):  
PAOLO FERRARIS ◽  
JOOHYUNG LEE ◽  
YULIYA LIERLER ◽  
VLADIMIR LIFSCHITZ ◽  
FANGKAI YANG
Keyword(s):  
Artificial Intelligence ◽  
Logic Programming ◽  
Logic Programs ◽  
Action Languages ◽  
First Order ◽  
National Conference ◽  
Theories Of Action ◽  
Causal Theories ◽  
Causal Logic ◽  
The Way

AbstractNonmonotonic causal logic, introduced by McCain and Turner (McCain, N. and Turner, H. 1997. Causal theories of action and change. In Proceedings of National Conference on Artificial Intelligence (AAAI), Stanford, CA, 460–465) became the basis for the semantics of several expressive action languages. McCain's embedding of definite propositional causal theories into logic programming paved the way to the use of answer set solvers for answering queries about actions described in such languages. In this paper we extend this embedding to nondefinite theories and to the first-order causal logic.

Algebraic Foundations of Logic Programming, I: The Distributive Lattice of Logic Programs

1990 ◽  
Vol 13 (3) ◽  
pp. 317-332
Author(s):  
Anil Hirani ◽  
V.S. Subrahmanian
Keyword(s):  
Distributive Lattice ◽  
Logic Program ◽  
Logic Programs ◽  
Intended Meaning ◽  
Zero Divisors ◽  
Order Language ◽  
Language L ◽  
General Logic ◽  
Pure Logic ◽  
Algebraic Properties

Given a logic program P, the operator TP associated with P is closely related to the intended meaning of P. Given a first order language L that is generated by finitely many non-logical symbols, our aim is to study the algebraic properties of the set {TP|P is a general logic program in language L} with certain operators on it. For the operators defined in this paper the resulting algebraic structure is a bounded distributive lattice. Our study extends (to the case of general logic programs), the work of Mancarella and Pedreschi who initiated a study of the algebraic properties of the space of pure logic programs. We study the algebraic properties of this set and identify the ideals and zero divisors. In addition, we prove that our algebra satisfies various non-extensibility conditions.

Sign in / Sign up

Export Citation Format

Share Document