Proof internalization in generalized Frege systems for classical logic

Yury Savateev

doi:10.1016/j.apal.2013.07.017

Proof internalization in generalized Frege systems for classical logic

Yury Savateev

Research output: Contribution to journal › Article › peer-review

Abstract

We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.

Original language	English
Pages (from-to)	340-356
Journal	Annals of Pure and Applied Logic
Volume	165
Issue number	1
DOIs	https://doi.org/10.1016/j.apal.2013.07.017
Publication status	Published - 13 Aug 2013

Access to Document

10.1016/j.apal.2013.07.017

Cite this

@article{9a1c74fe6a7a4af3b1249420754a6263,

title = "Proof internalization in generalized Frege systems for classical logic",

abstract = "We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.",

author = "Yury Savateev",

year = "2013",

month = aug,

day = "13",

doi = "10.1016/j.apal.2013.07.017",

language = "English",

volume = "165",

pages = "340--356",

journal = "Annals of Pure and Applied Logic",

issn = "0168-0072",

publisher = "Elsevier",

number = "1",

}

TY - JOUR

T1 - Proof internalization in generalized Frege systems for classical logic

AU - Savateev, Yury

PY - 2013/8/13

Y1 - 2013/8/13

N2 - We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.

AB - We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.

U2 - 10.1016/j.apal.2013.07.017

DO - 10.1016/j.apal.2013.07.017

M3 - Article

SN - 0168-0072

VL - 165

SP - 340

EP - 356

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 1

ER -

Proof internalization in generalized Frege systems for classical logic

Abstract

Access to Document

Fingerprint

Cite this