Working with ARMs: Complexity Results on Atomic Representations of Herbrand Models

An atomic representation of a Herbrand model (ARM) is a finite set of (not necessarily ground) atoms over a given Herbrand universe. Each ARM represents a possibly infinite Herbrand interpretation. This concept has emerged independently in different branches of computer science as a natural and useful generalization of the concept of finite Herbrand interpretation. It was shown that several recursively decidable problems on finite Herbrand models (or interpretations) remain decidable on ARMs.The following problems are essential when working with ARMs: Deciding the equivalence of two ARMs, deciding subsumption between ARMs, and evaluating clauses over ARMs. These problems were shown to be decidable, but their computational complexity has remained obscure so far. The previously published decision algorithms require exponential space. In this paper, we prove that all mentioned problems are coNP-complete.     

Compositional model-theoretic semantics for logic programs

We present a compositional model-theoretic semantics for logic programs, where the composition of programs is modelled by the composition of the admissible Herbrand models of the programs. An Herbrand model is admissible if it is supported by the assumption of a set of hypotheses. On one hand, the hypotheses supporting a model correspond to an open interpretation of the program intended to capture possible compositions with other programs. On the other hand, admissible models provide a natural model-theory for a form of hypothetical reasoning, called abduction. The application of admissibel models to programs with negation is discussed. Antonio Brogi: Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125 Pisa, ItalyResearch interests: Programming Language Design and Semantics, Logic Programming and Artificial Intelligence     

关于逻辑程序不动点语义的讨论

主要讨论逻辑程序中的最大不动点语义．证明了当Herbrand解释语义映射TP是保滤子交的,或者确定性程序中不含函数符号,或者它的每一个子句都满足：子句体的变量都在子句头中出现时,集合TP↓ω就是语义映射TP的最大不动点．然后定义了另一个Herbrand解释语义映射Fp将关于逻辑程序不动点语义的一些主要结论进行了推广．     

Characterizing minimal semantics-preserving slices of predicate-linear, free, liberal program schemas

A program schema defines a class of programs, all of which have identical statement structure, but whose functions and predicates may differ. A schema thus defines an entire class of programs according to how its symbols are interpreted. A subschema of a schema is obtained from a schema by deleting some of its statements. We prove that given a schema S which is predicate-linear, free and liberal, such that the true and false parts of every if predicate satisfy a simple additional condition, and a slicing criterion defined by the final value of a given variable after execution of any program defined by S, the minimal subschema of S which respects this slicing criterion contains all the function and predicate symbols ‘needed’ by the variable according to the data dependence and control dependence relations used in program slicing, which is the symbol set given by Weiser’s static slicing algorithm. Thus this algorithm gives predicate-minimal slices for classes of programs represented by schemas satisfying our set of conditions. We also give an example to show that the corresponding result with respect to the slicing criterion defined by termination behaviour is incorrect. This complements a result by the authors in which S was required to be function-linear, instead of predicate-linear.     

Herbrand theorems in arbitrary institutions

The basic logic programming semantic concepts, query, solutions, solution forms, and the fundamental results such as Herbrand theorems, are developed over any logical system, formalised as institution, by employing ‘institution-independent’ concepts of variable, substitution, quantifier, and atomic formulae. This sets semantical foundations for a uniform development of logic programming over a large variety of computing science logics, allowing for a clean combination of logic programming with other computing paradigms.     

Horn逻辑程序和形式文法之间的对应关系

The paper researches Horn logic programs with grammatical view. The correspondence between Horn logic programs and grammars is found. The method by which type-0 grammars generate the least Herbrand models of logic programs is found. The method by which Horn logic programs generate the languages of type-0 grammars is found.The characterization of Horn Logic programs that are semantically equavanent to type-2 grammars and type-3 grammars is found.     

Herbrand基上的启发式语义映射

一、引言 在逻辑程序中允许负文字出现,极大地增强了逻辑程序的表达能力,但同时也其语义定义带来了困难。可以说,至今还没有一种好的方法来定义一般逻辑程序的语义。     

PROLOG的说明性语义和过程性语义之间的循环论证

对关于PROLOG的说明性语义和过程性语义之间的关系的观点提出商榷。认为这两种语义之间存在循环论证,它反映了数理逻辑的模型论和证明论之间的循环论证。     

Explicit representation of terms defined by counter examples

Anti-unification guarantees the existence of a term which is an explicit representation of the most specific generalization of a collection of terms. This provides a formal basis for learning from examples. Here we address the dual problem of computing a generalization given a set of counter examples. Unlike learning from examples an explicit, finite representation for the generalization does not always exist. We show that the problem is decidable by providing an algorithm which, given an implicit representation will return a finite explicit representation or report that none exists. Applications of this result to the problem of negation as failure and to the representation of solutions to systems of equations and inequations are also mentioned.Research performed while visiting from the: Dept. of Computer Science, University of Melbourne, Parkville 3052, Australia.