Related papers: Proof terms for infinitary rewriting, progress rep…

Proof terms in term rewriting are a representation means for reduction sequences, and more in general for contraction activity, allowing to distinguish e.g simultaneous from sequential reduction. Proof terms for finitary, first-order,…

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting…

We introduce a generic presentation of 'syntactic objects built by mixed induction and coinduction' encompassing all standard kinds of infinitary terms, as well as derivation trees in non-wellfounded proof systems. We then define a notion…

Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive…

Logically constrained term rewriting is a rewriting framework that supports built-in data structures such as integers and bit vectors. Recently, constrained terms play a key role in various analyses and applications of logically constrained…

Representing a proof tree by a combinator term that reduces to the tree lets subtle forms of duplication within the tree materialize as duplicated subterms of the combinator term. In a DAG representation of the combinator term these…

We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way. The setup captures rewrite sequences of arbitrary ordinal length, but it has…

In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inference rules. We propose an extension of the Curry-Howard…

Verification methods based on SAT, SMT, and Theorem Proving often rely on proofs of unsatisfiability as a powerful tool to extract information in order to reduce the overall effort. For example a proof may be traversed to identify a minimal…

We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition…

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…

Cyclic proof theory breaks tradition by allowing certain infinite proofs: those that can be represented by a finite graph, while satisfying a soundness condition. We reconcile cyclic proofs with traditional finite proofs: we extend abstract…

We study an alternative model of infinitary term rewriting. Instead of a metric on terms, a partial order on partial terms is employed to formalise convergence of reductions. We consider both a weak and a strong notion of convergence and…

In logic there is a clear concept of what constitutes a proof and what not. A proof is essentially defined as a finite sequence of formulae which are either axioms or derived by proof rules from formulae earlier in the sequence.…

We introduce a sound and complete coinductive proof system for reachability properties in transition systems generated by logically constrained term rewriting rules over an order-sorted signature modulo builtins. A key feature of the…

Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving…

We introduce proof terms for string rewrite systems and, using these, show that various notions of equivalence on reductions known from the literature can be viewed as different perspectives on the notion of causal equivalence. In…

When a proposition has no proof in an inference system, it is sometimes useful to build a counter-proof explaining, step by step, the reason of this non-provability. In general, this counter-proof is a (possibly) infinite co-inductive proof…

This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including implicit arguments, are dropped during reduction of terms. We…

We investigate infinitary wellfounded systems for linear logic with fixed points, with transfinite branching rules indexed by some closure ordinal $\alpha$ for fixed points. Our main result is that provability in the system for some…