A semantic framework for proof evidence

DOI10.1007/s10817-016-9380-6zbMath1425.68371OpenAlexW2463991046MaRDI QIDQ1701039

Fabien Renaud, Zakaria Chihani, Dale A. Miller

Publication date: 22 February 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01390912/file/fpc-jar.pdf

zbMATH Keywords

intuitionistic logicclassical logicfocused proof systemsproof checkingfoundational proof certificatesproof certificates

Mathematics Subject Classification ID

Related Items (7)

Proof checking and logic programming ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Towards substructural property-based testing ⋮ Proof search and certificates for evidential transactions ⋮ Complexity of translations from resolution to sequent calculus ⋮ A general proof certification framework for modal logic ⋮ A proof theory for model checking

Uses Software

• Coq
• ML
• Isabelle/HOL
• Twelf
• LCF
• CLSAT
• DRAT-trim
• Teyjus
• YACC
• ELPI
• OpenTheory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The future of logic: foundation-independence
• Linear logic
• Proof and refutation in MALL as a game
• A focused approach to combining logics
• Producing and verifying extremely large propositional refutations
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A logical characterization of forward and backward chaining in the inverse method
• Focusing and polarization in linear, intuitionistic, and classical logics
• A compact representation of proofs
• Implementing tactics and tacticals in a higher-order logic programming language
• Theorem proving modulo
• Isabelle/HOL. A proof assistant for higher-order logic
• Autarkic computations in formal proofs
• Proof certificates for equality reasoning
• Edinburgh LCF. A mechanized logic of computation
• The foundation of a generic theorem prover
• The origins of structural operational semantics
• SMT proof checking using a logical framework
• Proofs without syntax
• Uniform proofs as a foundation for logic programming
• HOL-λσ: an intentional first-order expression of higher-order logic
• An open logical framework
• Programming with Higher-Order Logic
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Principles and implementation of deductive parsing
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• The Proof Certifier Checkers
• Focused Labeled Proof Systems for Modal Logic
• ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
• Classical and Intuitionistic Subexponential Logics Are Equally Expressive
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• A new constructive logic: classic logic
• Logic Programming with Focusing Proofs in Linear Logic
• A framework for defining logics
• The relative efficiency of propositional proof systems
• The Impact of the Lambda Calculus in Logic and Computer Science
• Foundational Proof Certificates in First-Order Logic
• Introduction to generalized type systems
• Oracle-based checking of untrusted software
• Call-by-Value  -calculus and LJQ
• Three models for the description of language
• A multi-focused proof system isomorphic to expansion proofs
• Proof Checking and Logic Programming
• Least and Greatest Fixed Points in Linear Logic
• Tools and Algorithms for the Construction and Analysis of Systems
• Solution to a problem of Ono and Komori
• The consistency of arithmetics

This page was built for publication: A semantic framework for proof evidence