DC Field
Value
Language
dc.contributor.author
Cerna, David M.
-
dc.contributor.author
Leitsch, Alexander
-
dc.contributor.author
Lolić, Anela
-
dc.date.accessioned
2023-01-19T14:05:45Z
-
dc.date.available
2023-01-19T14:05:45Z
-
dc.date.issued
2021-06
-
dc.identifier.citation
<div class="csl-bib-body"> <div class="csl-entry">Cerna, D. M., Leitsch, A., &#38; Lolić, A. (2021). Schematic Refutations of Formula Schemata. <i>Journal of Automated Reasoning</i>, <i>65</i>(5), 599–645. https://doi.org/10.1007/s10817-020-09583-8</div> </div>
-
dc.identifier.issn
0168-7433
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/141768
-
dc.description.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.
en
dc.language.iso
en
-
dc.publisher
SPRINGER
-
dc.relation.ispartof
Journal of Automated Reasoning
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
Software
en
dc.subject
Artificial Intelligence
en
dc.subject
Computational Theory and Mathematics
en
dc.title
Schematic Refutations of Formula Schemata
en
dc.type
Artikel
de
dc.type
Article
en
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.description.startpage
599
-
dc.description.endpage
645
-
dcterms.dateSubmitted
2019-12-19
-
dc.rights.holder
© The Author(s) 2020
-
dc.type.category
Original Research Article
-
tuw.container.volume
65
-
tuw.container.issue
5
-
tuw.journal.peerreviewed
true
-
tuw.peerreviewed
true
-
tuw.researchTopic.id
X1
-
tuw.researchTopic.name
außerhalb der gesamtuniversitären Forschungsschwerpunkte
-
tuw.researchTopic.value
100
-
dcterms.isPartOf.title
Journal of Automated Reasoning
-
tuw.publication.orgunit
E104-02 - Forschungsbereich Computational Logic
-
tuw.publication.orgunit
E192-05 - Forschungsbereich Theory and Logic
-
tuw.publisher.doi
10.1007/s10817-020-09583-8
-
dc.date.onlinefirst
2020-11-19
-
dc.identifier.eissn
1573-0670
-
dc.identifier.libraryid
AC17203490
-
dc.description.numberOfPages
47
-
tuw.author.orcid
0000-0002-6352-603X
-
tuw.author.orcid
0000-0002-4753-7302
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
wb.sci
true
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1010
-
wb.facultyfocus
Diskrete Mathematik und Geometrie
de
wb.facultyfocus
Discrete Mathematics and Geometry
en
wb.facultyfocus.faculty
E100
-
item.languageiso639-1
en
-
item.openairetype
research article
-
item.grantfulltext
open
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_2df8fbb1
-
item.openaccessfulltext
Open Access
-
crisitem.author.dept
E185 - Institut für Computersprachen
-
crisitem.author.dept
E192-05 - Forschungsbereich Theory and Logic
-
crisitem.author.dept
E192-02 - Forschungsbereich Databases and Artificial Intelligence
-
crisitem.author.parentorg
E180 - Fakultät für Informatik
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
Appears in Collections:
Article
Thumbnail
Fulltext (Version of Record (published version))
Adobe PDF
(683.03 kB)
Open Access CC BY 4.0
Show simple item record

Page view(s)

259
checked on Nov 23, 2023

Download(s)

43
checked on Nov 23, 2023

Google ScholarTM

Check