Related papers: Coinduction in Uniform: Foundations for Corecursiv…

This paper presents Abduction and Argumentation as two principled forms for reasoning, and fleshes out the fundamental role that they can play within Machine Learning. It reviews the state-of-the-art work over the past few decades on the…

We present automated theorem provers for the first-order logic of here and there (HT). They are based on a native sequent calculus for the logic of HT and an axiomatic embedding of the logic of HT into intuitionistic logic. The analytic…

Guarded recursion is a powerful modal approach to recursion that can be seen as an abstract form of step-indexing. It is currently used extensively in separation logic to model programming languages with advanced features by solving domain…

We introduce an operational rewriting-based semantics for strictly positive nested higher-order (co)inductive types. The semantics takes into account the "limits" of infinite reduction sequences. This may be seen as a refinement and…

After surveying classical results, we introduce a generalized notion of inference system to support structural recursion on non-well-founded data types. Besides axioms and inference rules with the usual meaning, a generalized inference…

This paper studies fundamental questions concerning category-theoretic models of induction and recursion. We are concerned with the relationship between well-founded and recursive coalgebras for an endofunctor. For monomorphism preserving…

Logical frameworks provide natural and direct ways of specifying and reasoning within deductive systems. The logical framework LF and subsequent developments focus on finitary proof systems, making the formalization of circular proof…

We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number…

Constraint Logic Programming (CLP) and Hereditary Harrop formulas (HH) are two well known ways to enhance the expressivity of Horn clauses. In this paper, we present a novel combination of these two approaches. We show how to enrich the…

Building on the successes of satisfiability modulo theories (SMT), Bj{\o}rner et al. initiated a research programme advocating Horn constraints as a suitable basis for automatic program verification. The notion of first-order constrained…

While reasoning in a logic extending a complete Boolean basis is coNP-hard, restricting to conjunctive fragments of modal languages sometimes allows for tractable reasoning even in the presence of greatest fixpoints. One such example is the…

Theorem provers are tools that help users to write machine readable proofs. Some of this tools are also interactive. The need of such softwares is increasing since they provide proofs that are more certified than the hand written ones. Agda…

It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of models into a constant domain. This makes it an interesting…

In this paper, we give two proofs of the wellfoundedness of recursive notation systems for $\Pi_N$-reflecting ordinals. One is based on $\Pi_{N-1}^0$-inductive definitions, and the other is based on distinguished classes.

This paper extends the fibrational approach to induction and coinduction pioneered by Hermida and Jacobs, and developed by the current authors, in two key directions. First, we present a dual to the sound induction rule for inductive types…

This paper is concerned with a class of algorithms that perform exhaustive search on propositional knowledge bases. We show that each of these algorithms defines and generates a propositional language. Specifically, we show that the trace…

In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program…

Many semantical aspects of programming languages, such as their operational semantics and their type assignment calculi, are specified by describing appropriate proof systems. Recent research has identified two proof-theoretic features that…

In the article 'Ordinal Logics and the Characterizations of the Informal Concept of Proof', Georg Kreisel poses the problem of assigning unique notations to recursive ordinals, and additionally suggests that the methods which are developed…

We introduce an extension of first-order logic that comes equipped with additional predicates for reasoning about an abstract state. Sequents in the logic comprise a main formula together with pre- and postconditions in the style of Hoare…