Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized delta-Rule but Without Skolemization

Simple item page
dc.creatorWirth, Claus-Peter
dc.date2009-02-21
dc.date.accessioned2026-07-07T12:45:27Z
dc.date.available2026-07-07T12:45:27Z
dc.descriptionWe present a combination of raising, explicit variable dependency representation, the liberalized delta-rule, and preservation of solutions for first-order deductive theorem proving. Our main motivation is to provide the foundation for our work on inductive theorem proving, where the preservation of solutions is indispensable.
dc.descriptionii + 40 pages
dc.identifierhttps://arxiv.org/abs/0902.3730
dc.identifierhttp://arxiv.org/abs/0902.3730
dc.identifierCaferra, R. and Salzer, G., eds., Automated Deduction in Classical and Non-Classical Logics (FTP'98), LNAI 1761, pp. 283-298, Springer, 2000
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/221090
dc.subjectArtificial Intelligence
dc.subjectLogic in Computer Science
dc.titleFull First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized delta-Rule but Without Skolemization
dc.typetext

Files

Collections

arXiv