IMI-BAS
 

BulDML at Institute of Mathematics and Informatics >
ITHEA >
International Journal ITA >
2003 >
Volume 10 Number 4 >

Please use this identifier to cite or link to this item: http://hdl.handle.net/10525/967

Title: Admissible Substitutions in Sequent Calculi
Authors: Lyaletski, Alexander
Keywords: Completeness
First-Order Logic
Quantifier Rule
Sequent Calculus
Skolemization
Soundness
Issue Date: 2003
Publisher: Institute of Information Theories and Applications FOI ITHEA
Abstract: For first-order classical logic a new notion of admissible substitution is defined. This notion allows optimizing the procedure of the application of quantifier rules when logical inference search is made in sequent calculi. Our objective is to show that such a computer-oriented sequent technique may be created that does not require a preliminary skolemization of initial formulas and that is efficiently comparable with methods exploiting the skolemization. Some results on its soundness and completeness are given.
URI: http://hdl.handle.net/10525/967
ISSN: 1313-0463
Appears in Collections:Volume 10 Number 4

Files in This Item:

File Description SizeFormat
ijita10-4-p05.pdf64.09 kBAdobe PDFView/Open

 



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

 

Valid XHTML 1.0! DSpace Software Copyright © 2002-2009  The DSpace Foundation - Feedback