Full first-order sequent and tableau calculi with preservation of solutions and the liberalized delta-rule but without Skolemization

Authors
Wirth, CP
Citation
Cp. Wirth, Full first-order sequent and tableau calculi with preservation of solutions and the liberalized delta-rule but without Skolemization, LECT N A I, 1761, 2000, pp. 282-297
Citations number
20
Categorie Soggetti
Current Book Contents
Journal title
AUTOMATED DEDUCTION IN CLASSICAL AND NON-CLASSICAL LOGICS → ACNP
ISSN journal
03029743
Volume
1761
Year of publication
2000
Pages
282 - 297
Database
ISI
SICI code
0302-9743(2000)1761:<282:FFSATC>2.0.ZU;2-S
Abstract
We present a combination of raising, explicit variable dependency represent ation, the liberalized delta -rule, and preservation of solutions for first -order deductive theorem proving. Our main motivation is to pro vide the fo undation for our work on inductive theorem proving.