Index Sets for Finite Normal Predicate Logic Programs with Function Symbols

On the complexity of index sets for finite predicate logic programs which allow function symbols

Journal of Logic and Computation ◽

10.1093/logcom/exaa005 ◽

2020 ◽

Vol 30 (1) ◽

pp. 107-156

Author(s):

D Cenzer ◽

V W Marek ◽

J B Remmel

Keyword(s):

Positive Integer ◽

Predicate Logic ◽

Stable Model ◽

Logic Programs ◽

Index Set ◽

Natural Properties ◽

Index Sets ◽

Predicate Language ◽

Arithmetic Hierarchy ◽

Stable Models

Abstract We study the recognition problem in the metaprogramming of finite normal predicate logic programs. That is, let $\mathcal{L}$ be a computable first-order predicate language with infinitely many constant symbols and infinitely many $n$-ary predicate symbols and $n$-ary functions symbols for all $n \geq 1$. Then we can effectively list all the finite normal predicate logic programs $Q_0,Q_1,\ldots $ over $\mathcal{L}$. Given some property $\mathcal{P}$ of finite normal predicate logic programs over $\mathcal{L}$, we define the index set $I_{\mathcal{P}}$ to be the set of indices $e$ such that $Q_e$ has property $\mathcal{P}$. We classify the complexity of the index set $I_{\mathcal{P}}$ within the arithmetic hierarchy for various natural properties of finite predicate logic programs. For example, we determine the complexity of the index sets relative to all finite predicate logic programs and relative to certain special classes of finite predicate logic programs of properties such as (i) having no stable models, (ii) having no recursive stable models, (iii) having at least one stable model, (iv) having at least one recursive stable model, (v) having exactly $c$ stable models for any given positive integer $c$, (vi) having exactly $c$ recursive stable models for any given positive integer $c$, (vii) having only finitely many stable models, (viii) having only finitely many recursive stable models, (ix) having infinitely many stable models and (x) having infinitely many recursive stable models.

Download Full-text

Transformation of Logic Programs

Handbook of Logic in Artificial Intelligence and Logic Programming: Volume 5: Logic Programming ◽

10.1093/oso/9780198537922.003.0013 ◽

1998 ◽

Author(s):

Alberto Pettorossi ◽

Maurizio Proietti

Keyword(s):

Program Transformation ◽

Predicate Logic ◽

Software Systems ◽

Second Phase ◽

Logic Programs ◽

Transformation Approach ◽

Basic Transformation ◽

Initial Program ◽

Two Phases ◽

Efficient Program

Program transformation is a methodology for deriving correct and efficient programs from specifications. In this chapter, we will look at the so called ’rules + strategies’ approach, and we will report on the main techniques which have been introduced in the literature for that approach, in the case of logic programs. We will also present some examples of program transformation, and we hope that through those examples the reader may acquire some familiarity with the techniques we will describe. The program transformation approach to the development of programs has been first advocated in the case of functional languages by Burstall and Darlington [1977]. In that seminal paper the authors give a comprehensive account of some basic transformation techniques which they had already presented in [Darlington, 1972; Burstall and Darlington, 1975]. Similar techniques were also developed in the case of logic languages by Clark and Sickel [1977], and Hogger [1981], who investigated the use of predicate logic as a language for both program specification and program derivation. In the transformation approach the task of writing a correct and efficient program is realized in two phases. The first phase consists in writing an initial, maybe inefficient, program whose correctness can easily be shown, and the second phase, possibly divided into various subphases, consists in transforming the initial program with the objective of deriving a new program which is more efficient. The separation of the correctness concern from the efficiency concern is one of the major advantages of the transformation methodology. Indeed, using this methodology one may avoid some difficulties often encountered in other approaches. One such difficulty, which may occur when following the stepwise refinement approach, is the design of the invariant assertions, which may be quite intricate, especially when developing very efficient programs. The experience gained during the past two decades or so shows that the methodology of program transformation is very valuable and attractive, in particular for the task of programming ‘in the small’, that is, for writing single modules of large software systems.

Download Full-text

Generalized Disjunctive Well-Founded Semantics for Logic Programs

10.21236/ada232064 ◽

1990 ◽

Cited By ~ 19

Author(s):

Chitta Baral ◽

Jorge Lobo ◽

Jack Minker

Keyword(s):

Logic Programs

Download Full-text

Logical Decision Problems and Complexity of Logic Programs

Fundamenta Informaticae ◽

10.3233/fi-1987-10102 ◽

1987 ◽

Vol 10 (1) ◽

pp. 1-33

Author(s):

Egon Börger ◽

Ulrich Löwen

Keyword(s):

Fixed Point ◽

Computational Complexity ◽

Decision Problem ◽

Decision Problems ◽

Complexity Classes ◽

Logic Programs ◽

Finite Structures ◽

Syntactic Restrictions

We survey and give new results on logical characterizations of complexity classes in terms of the computational complexity of decision problems of various classes of logical formulas. There are two main approaches to obtain such results: The first approach yields logical descriptions of complexity classes by semantic restrictions (to e.g. finite structures) together with syntactic enrichment of logic by new expressive means (like e.g. fixed point operators). The second approach characterizes complexity classes by (the decision problem of) classes of formulas determined by purely syntactic restrictions on the formation of formulas.

Download Full-text

Y-Logic: A Framework for Reasoning About Chameleonic Programs with Inconsistent Completions

Fundamenta Informaticae ◽

10.3233/fi-1990-13405 ◽

1990 ◽

Vol 13 (4) ◽

pp. 465-483

Author(s):

V.S. Subrahmanian

Keyword(s):

Classical Logic ◽

Logic Program ◽

Logic Programs ◽

Large Subset ◽

General Logic ◽

Traditional Sense

Large logic programs are normally designed by teams of individuals, each of whom designs a subprogram. While each of these subprograms may have consistent completions, the logic program obtained by taking the union of these subprograms may not. However, the resulting program still serves a useful purpose, for a (possibly) very large subset of it still has a consistent completion. We argue that “small” inconsistencies may cause a logic program to have no models (in the traditional sense), even though it still serves some useful purpose. A semantics is developed in this paper for general logic programs which ascribes a very reasonable meaning to general logic programs irrespective of whether they have consistent (in the classical logic sense) completions.

Download Full-text