Related papers: A Prolog Program for Bottom-up Evaluation
A range of methodologies and techniques are available to guide the design and implementation of language extensions and domain-specific languages. A simple yet powerful technique is based on source-to-source transformations interleaved…
In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this…
This article shows a correspondence between abstract interpretation of imperative programs and the refinement calculus: in the refinement calculus, an abstract interpretation of a program is a specification which is a function. This…
ProFIT is an extension of Standard Prolog with Features, Inheritance and Templates. ProFIT allows the programmer or grammar developer to declare an inheritance hierarchy, features and templates. Sorted feature terms can be used in ProFIT…
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…
A simple mathematical definition of the 4-port model for pure Prolog is given. The model combines the intuition of ports with a compact representation of execution state. Forward and backward derivation steps are possible. The model…
Tabled evaluation is an implementation technique that solves some problems of traditional Prolog systems in dealing with recursion and redundant computations. Most tabling engines determine if a tabled subgoal will produce or consume…
Convex polyhedral abstractions of logic programs have been found very useful in deriving numeric relationships between program arguments in order to prove program properties and in other areas such as termination and complexity analysis. We…
ProbLog is a popular probabilistic logic programming language/tool, widely used for applications requiring to deal with inherent uncertainties in structured domains. In this paper we study connections between ProbLog and a variant of…
We discuss the syntax and semantics of relational Horn logic (RHL) and partial Horn logic (PHL). RHL is an extension of the Datalog programming language that allows introducing and equating variables in conclusions. PHL is a syntactic…
We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We propose a new algorithmic method for synthesizing loop…
$\{log\}$ is a programming language at the intersection of Constraint Logic Programming, set programming and declarative programming. But $\{log\}$ is also a satisfiability solver for a theory of finite sets and finite binary relations.…
Higher-order logic programming is an interesting extension of traditional logic programming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higher-order characteristics are indeed…
We establish a translation between a formalism for dynamic programming over hypergraphs and the computation of semiring-based provenance for Datalog programs. The benefit of this translation is a new method for computing provenance for a…
Epistemic Logic Programs (ELPs), extend Answer Set Programming (ASP) with epistemic operators. The semantics of such programs is provided in terms of world views, which are sets of belief sets, i.e., syntactically, sets of sets of atoms.…
PROMELA (Process Meta Language) is a high-level specification language designed for modeling interactions in distributed systems. PROMELA is used as the input language for the model checker SPIN (Simple Promela INterpreter). The main…
We discuss how to implement backjumping (or intelligent backtracking) in Prolog programs by means of exception handling. This seems impossible in a general case. We provide two solutions. One works for binary programs; in a general case it…
Type-preserving (or typed) compilation uses typing derivations to certify correctness properties of compilation. We have designed and implemented a type-preserving compiler for a simply-typed dialect of Prolog we call T-Prolog. The crux of…
We present a novel definition of an algorithm and its corresponding algorithm language called CoLweb. The merit of CoLweb [1] is that it makes algorithm design so versatile. That is, it forces us to a high-level, proof-carrying,…
Abstract machines for the strong evaluation of lambda-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper…