We observe today a large diversity of proof systems. This diversity has the negative
consequence that a lot of theorems are proved many times. Unlike programming languages …

Theorem provers produce evidence of proof in many different formats, such as proof scripts,
natural deductions, resolution refutations, Herbrand expansions, and equational rewritings …

Dedukti is a logical framework based on the lambda-Pi-calculus modulo rewriting, which
extends the lambda-Pi-calculus with rewrite rules. In this paper, we show how to translate …

Focused proofs are sequent calculus proofs that group inference rules into alternating
positive and negative phases. These phases can then be used to define macro-level …

Hybrid deduction–refutation systems are deductive systems intended to derive both valid
and non-valid, ie, semantically refutable, formulae of a given logical system, by employing …

Modal μ-calculus is one of the central languages of logic and verification, whose study
involves notoriously complex objects: automata over infinite structures on the model …

Several deductive formalisms (eg, sequent, nested sequent, labeled sequent, hyperse-quent
calculi) have been used in the literature for the treatment of modal logics, and some …

Different theorem provers work within different formalisms and paradigms, and therefore
produce various incompatible proof objects. Currently there is a big effort to establish …

Abstract The Foundational Proof Certificate (FPC) framework can be used to define the
semantics of a wide range of proof evidence. For example, such definitions exist for a …

In a world where trusting software systems is problematic, formal methods and formal proofs
should be able to help. Proof checking can play an important role in establishing trust since …