Abstract Eunoia is a logical framework designed for specifying the proofs and proof systems of SMT solvers, namely cvc5 . We present a translation from a core fragment of Eunoia to the $$\lambda \Pi $$ λ Π -calculus modulo rewriting as implemented by the LambdaPi proof assistant. The translation is implemented by our tool , which we use for generating LambdaPi encodings of (a) a large fragment of the Cooperating Proof Calculus (CPC), the Eunoia signature defining cvc5 ’s proof system, and (b) proofs produced by cvc5 on problems from various fragments of SMT-LIB.

Focusing and selection are techniques that shrink the proof-search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atomic formula can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory and the related framework called superdeduction; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof-search space.

Focusing and selection are techniques that shrink the proof search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atom can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof search space.

Superdeduction is a formalism closely related to deduction modulo which permits to enrich a deduction system - especially a first-order one such as natural deduction or sequent calculus - with new inference rules automatically computed from the presentation of a theory. We give a natural encoding from every functional pure type system (PTS) into superdeduction by defining an appropriate first-order theory. We prove that this translation is correct and conservative, showing a correspondence between valid typing judgments in the PTS and provable sequents in the corresponding superdeductive system. As a byproduct, we also introduce the superdeductive sequent calculus for intuitionistic logic, which was until now only defined for classical logic. We show its equivalence with the superdeductive natural deduction. This implies that superdeduction can be easily used as a logical framework. These results lead to a better understanding of the implementation and the automation of proof search for PTS, as well as to more cooperation between proof assistants.