Schematic Refutations of Formula Schemata

Cerna, David M.; Leitsch, Alexander; Lolić, Anela

doi:10.1007/s10817-020-09583-8

Record link:

http://hdl.handle.net/20.500.12708/141768

Title:

Schematic Refutations of Formula Schemata

Citation:

Cerna, D. M., Leitsch, A., & Lolić, A. (2021). Schematic Refutations of Formula Schemata. Journal of Automated Reasoning, 65(5), 599–645. https://doi.org/10.1007/s10817-020-09583-8

Publisher DOI:

10.1007/s10817-020-09583-8

CatalogPlus:

AC17203490

Publication Type:

Article - Original Research Article

Language:

English

Authors:

Cerna, David M.
Leitsch, Alexander
Lolić, Anela

Organisational Unit:

E104-02 - Forschungsbereich Computational Logic
E192-05 - Forschungsbereich Theory and Logic

Journal:

Journal of Automated Reasoning

ISSN:

0168-7433

Date (published):

Jun-2021

Number of Pages:

Publisher:

SPRINGER

Peer reviewed:

Yes

Keywords:

Software; Artificial Intelligence; Computational Theory and Mathematics

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.

Research Areas:

außerhalb der gesamtuniversitären Forschungsschwerpunkte: 100%

Science Branch:

Mathematik

License:

CC BY 4.0