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

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

We 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.
ii + 40 pages

Keywords

Artificial Intelligence, Logic in Computer Science

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/221090

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/0902.3730
 http://arxiv.org/abs/0902.3730
 Caferra, R. and Salzer, G., eds., Automated Deduction in Classical and Non-Classical Logics (FTP'98), LNAI 1761, pp. 283-298, Springer, 2000

Collections

arXiv