相关论文: A Refinement Calculus for Logic Programs

Intuitionistic grammar logics fuse constructive and multi-modal reasoning while permitting the use of converse modalities, serving as a generalization of standard intuitionistic modal logics. In this paper, we provide definitions of these…

Definite descriptions are expressions of the form "the unique $x$ satisfying property $C$," which allow reference to objects through their distinguishing characteristics. They play a crucial role in ontology and query languages, offering an…

There has recently been an increasing interest in declarative data analysis, where analytic tasks are specified using a logical language, and their implementation and optimisation are delegated to a general-purpose query engine. Existing…

The work relates to the automatic generation of logical specifications, considered as sets of temporal logic formulas, extracted directly from developed software models. The extraction process is based on the assumption that the whole…

Recent research in extensions of Answer Set Programming has included a renewed interest in the language of Epistemic Specifications, which adds modal operators K ("known") and M ("may be true") to provide for more powerful introspective…

In this paper, a possibilistic disjunctive logic programming approach for modeling uncertain, incomplete and inconsistent information is defined. This approach introduces the use of possibilistic disjunctive clauses which are able to…

In this work we present work in progress on functionality duplication detection in logic programs. Eliminating duplicated functionality recently became prominent in context of refactoring. We describe a quantitative approach that allows to…

An equational logic program is a set of directed equations or rules, which are used to compute in the obvious way (by replacing equals with ``simpler'' equals). We present static analysis techniques for efficient equational logic…

We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of ReLoC is its refinement judgment $e…

Disjunctive finitary programs are a class of logic programs admitting function symbols and hence infinite domains. They have very good computational properties, for example ground queries are decidable while in the general case the stable…

The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem-provers, thus providing a…

In prior work, we showed that logic programming compilation can be given a proof-theoretic justification for generic abstract logic programming languages, and demonstrated this technique in the case of hereditary Harrop formulas and their…

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…

Recursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called flexible coinduction, to express a variety of intermediate interpretations,…

We introduce DeepProbLog, a probabilistic logic programming language that incorporates deep learning by means of neural predicates. We show how existing inference and learning techniques can be adapted for the new language. Our experiments…

The sequent calculus is a formalism for proving validity of statements formulated in First-Order Logic. It is routinely used in computer science modules on mathematical logic. Formal proofs in the sequent calculus are finite trees obtained…

We design various logics for proving hyper properties of iterative programs by application of abstract interpretation principles. In part I, we design a generic, structural, fixpoint abstract interpreter parameterized by an algebraic…

We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the…

Many interesting and useful symbolic computation algorithms manipulate mathematical expressions in mathematically meaningful ways. Although these algorithms are commonplace in computer algebra systems, they can be surprisingly difficult to…

Checking the compliance of software against laws, regulations and contracts is increasingly important and costly as the embedding of software into societal practices is becoming more pervasive. Moreover, the digitalised services provided by…