Schematic Refutations of Formula Schemata
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F21%3A00534055" target="_blank" >RIV/67985807:_____/21:00534055 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/s10817-020-09583-8" target="_blank" >http://dx.doi.org/10.1007/s10817-020-09583-8</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/s10817-020-09583-8" target="_blank" >10.1007/s10817-020-09583-8</a>
Alternative languages
Result language
angličtina
Original language name
Schematic Refutations of Formula Schemata
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2021
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Journal of Automated Reasoning
ISSN
0168-7433
e-ISSN
1573-0670
Volume of the periodical
65
Issue of the periodical within the volume
5
Country of publishing house
NL - THE KINGDOM OF THE NETHERLANDS
Number of pages
47
Pages from-to
599-645
UT code for WoS article
000657362400001
EID of the result in the Scopus database
2-s2.0-85096320647