相关论文: Nominal Logic Programming

An attempt at unifying logic and functional programming is reported. As a starting point, we take the view that "logic programs" are not about logic but constitute inductive definitions of sets and relations. A skeletal language design…

Every definite logic program has as its meaning a least Herbrand model with respect to the program-independent ordering "set-inclusion". In the case of normal logic programs there do not exist least models in general. However, according to…

We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which…

This paper presents matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the patterns, are constructed using variables, symbols, connectives…

Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such…

We provide here a computational interpretation of first-order logic based on a constructive interpretation of satisfiability w.r.t. a fixed but arbitrary interpretation. In this approach the formulas themselves are programs. This contrasts…

The emerging field of Nominal Computation Theory is concerned with the theory of Nominal Sets and its applications to Computer Science. We investigate here the impact of nominal sets on the definition of Cellular Automata and on their…

Nominalistic Logic (NL) is a new presentation of Paul Gilmore's Intensional Type Theory (ITT) as a sequent calculus together with a succinct nominalization axiom (N) that permits names of predicates as individuals in certain cases. The…

We define a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable a, the domain of the model contains an element [[a]] which…

Semantics of logic programs has been given by proof theory, model theory and by fixpoint of the immediate-consequence operator. If clausal logic is a programming language, then it should also have a compositional semantics. Compositional…

The idea of using unfolding as a way of computing a program semantics has been applied successfully to logic programs and has shown itself a powerful tool that provides concrete, implementable results, as its outcome is actually source…

Non deterministic applications arise in many domains, including, stochastic optimization, multi-objectives optimization, stochastic planning, contingent stochastic planning, reinforcement learning, reinforcement learning in partially…

Nominal abstract syntax and higher-order abstract syntax provide a means for describing binding structure which is higher-level than traditional techniques. These approaches have spawned two different communities which have developed along…

We propose a purely extensional semantics for higher-order logic programming. In this semantics program predicates denote sets of ordered tuples, and two predicates are equal iff they are equal as sets. Moreover, every program has a unique…

Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In PNL, the forall-quantifier or lambda-binder are just…

We propose a modular method for proving termination of general logic programs (i.e., logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider…

Over the past thirty years, there has been significant progress in developing general-purpose, language-based approaches to incremental computation, which aims to efficiently update the result of a computation when an input is changed. A…

Constructor-Based Conditional Rewriting Logic is a general framework for integrating first-order functional and logic programming which gives an algebraic semantics for non-deterministic functional-logic programs. In the context of this…

Part of the theory of logic programming and nonmonotonic reasoning concerns the study of fixed-point semantics for these paradigms. Several different semantics have been proposed during the last two decades, and some have been more…

This paper analyses the declarative readings of logic programming. Logic programming - and negation as failure - has no unique declarative reading. One common view is that logic programming is a logic for default reasoning, a sub-formalism…