Schematic Refutations of Formula Schemata

David Cerna; Alexander Leitsch; Anela Lolic

doi:10.1007/s10817-020-09583-8

Schematic Refutations of Formula Schemata

David Cerna
, Alexander Leitsch
, Anela Lolic

Research Institute for Symbolic Computation

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

Abstract

Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.

Original language	English
Pages (from-to)	599-645
Number of pages	47
Journal	Journal of Automated Reasoning
Issue number	5
DOIs	https://doi.org/10.1007/s10817-020-09583-8
Publication status	Published - 2020

Fields of science

101 Mathematics
101001 Algebra
101005 Computer algebra
101009 Geometry
101012 Combinatorics
101013 Mathematical logic
101020 Technical mathematics

JKU Focus areas

Digital Transformation

Access to Document

10.1007/s10817-020-09583-8

Cite this

@article{b402b21889254f51b6e0d86d11497df8,

title = "Schematic Refutations of Formula Schemata",

abstract = "Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.",

author = "David Cerna and Alexander Leitsch and Anela Lolic",

year = "2020",

doi = "10.1007/s10817-020-09583-8",

language = "English",

pages = "599--645",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "5",

}

TY - JOUR

T1 - Schematic Refutations of Formula Schemata

AU - Cerna, David

AU - Leitsch, Alexander

AU - Lolic, Anela

PY - 2020

Y1 - 2020

N2 - Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.

AB - Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.

UR - https://www.scopus.com/pages/publications/85096320647

U2 - 10.1007/s10817-020-09583-8

DO - 10.1007/s10817-020-09583-8

M3 - Article

SN - 0168-7433

SP - 599

EP - 645

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 5

ER -

Schematic Refutations of Formula Schemata

Abstract

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this