Z Chihani, D Miller, F Renaud - Journal of Automated Reasoning, 2017 - Springer
Theorem provers produce evidence of proof in many different formats, such as proof scripts, natural deductions, resolution refutations, Herbrand expansions, and equational rewritings …
A Assaf, G Burel - arXiv preprint arXiv:1507.08720, 2015 - arxiv.org
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 …
D Miller, M Volpe - Logic for Programming, Artificial Intelligence, and …, 2015 - Springer
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 …
A Doumane, D Baelde, L Hirschi, A Saurin - Proceedings of the 31st …, 2016 - dl.acm.org
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 …
S Marin, D Miller, M Volpe - 11th conference on" Advances in Modal …, 2016 - hal.science
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 …
Z Chihani, T Libal, G Reis - … Reasoning with Analytic Tableaux and Related …, 2015 - Springer
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 …
D Miller - Proceedings of the 17th International Symposium on …, 2015 - dl.acm.org
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 …