A semantic framework for proof evidence
type: Item
instance of: scholarly article
title: A semantic framework for proof evidence
zbMATH Open document ID: 1425.68371
author: Zakaria Chihani
author: Fabien Renaud
author: Dale Miller
published in: Journal of Automated Reasoning
publication date: 2018-02-22T00:00:00Z
full work available at URL: fpc-jar.pdf
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 6842147
zbMATH Keywords: proof certificates
zbMATH Keywords: proof checking
zbMATH Keywords: focused proof systems
zbMATH Keywords: classical logic
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: foundational proof certificates
describes a project that uses: CLSAT
describes a project that uses: DRAT-trim
describes a project that uses: Teyjus
describes a project that uses: ELPI
describes a project that uses: Coq
describes a project that uses: Twelf
describes a project that uses: LCF
describes a project that uses: ML
describes a project that uses: Isabelle/HOL
describes a project that uses: YACC
describes a project that uses: OpenTheory
MaRDI profile type: Publication
OpenAlex ID: W2463991046
cites work: Logic Programming with Focusing Proofs in Linear Logic
cites work: A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
cites work: Least and Greatest Fixed Points in Linear Logic
cites work: The Impact of the Lambda Calculus in Logic and Computer Science
cites work: Autarkic computations in formal proofs
cites work: Introduction to generalized type systems
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: A compact representation of proofs
cites work: Classical and Intuitionistic Subexponential Logics Are Equally Expressive
cites work: A multi-focused proof system isomorphic to expansion proofs
cites work: A logical characterization of forward and backward chaining in the inverse method
cites work: The relative efficiency of propositional proof systems
cites work: The Proof Certifier Checkers
cites work: Proof certificates for equality reasoning
cites work: Foundational Proof Certificates in First-Order Logic
cites work: Producing and verifying extremely large propositional refutations
cites work: Three models for the description of language
cites work: Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
cites work: Q4842975
cites work: Q5667469
cites work: Proof and refutation in MALL as a game
cites work: Q3086782
cites work: HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
cites work: Theorem proving modulo
cites work: ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
cites work: Call-by-Value -calculus and LJQ
cites work: Implementing tactics and tacticals in a higher-order logic programming language
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Q3743300
cites work: The consistency of arithmetics
cites work: Linear logic
cites work: A new constructive logic: classic logic
cites work: Q3994895
cites work: Q4754492
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: A framework for defining logics
cites work: An open logical framework
cites work: Proofs without syntax
cites work: Q3774923
cites work: Focusing and polarization in linear, intuitionistic, and classical logics
cites work: A focused approach to combining logics
cites work: Q5726697
cites work: Q5271422
cites work: Proof Checking and Logic Programming
cites work: Programming with higher-order logic.
cites work: Uniform proofs as a foundation for logic programming
cites work: From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
cites work: Focused Labeled Proof Systems for Modal Logic

A semantic framework for proof evidence (cites work)
cites work: Oracle-based checking of untrusted software

A semantic framework for proof evidence (cites work)
cites work: Isabelle/HOL. A proof assistant for higher-order logic

A semantic framework for proof evidence (cites work)
cites work: The foundation of a generic theorem prover

A semantic framework for proof evidence (cites work)
cites work: Q3992706

A semantic framework for proof evidence (cites work)
cites work: The origins of structural operational semantics

A semantic framework for proof evidence (cites work)
cites work: Q5559220

A semantic framework for proof evidence (cites work)
cites work: The future of logic: foundation-independence

A semantic framework for proof evidence (cites work)
cites work: Principles and implementation of deductive parsing

A semantic framework for proof evidence (cites work)
cites work: Solution to a problem of Ono and Komori

A semantic framework for proof evidence (cites work)
cites work: Q3969890

A semantic framework for proof evidence (cites work)
cites work: SMT proof checking using a logical framework

A semantic framework for proof evidence (cites work)
cites work: Q4499084

A semantic framework for proof evidence (cites work)
cites work: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs

A semantic framework for proof evidence (DOI)
DOI: 10.1007/S10817-016-9380-6