A First Order System with Finite Choice of Premises
作者： A Guglielmi , K Bruennler
DOI:
关键词:
摘要: We present an inference system for classical first order logic in which each rule, including the cut, only has a finite set of premises to choose from. The main conceptual contribution this paper is possibility separating different sources infinite choice, happen be entangled traditional cut rule.
bath.ac.uk参考文章(13)
Charles Stewart, Phiniki Stouppa, A Systematic Proof Theory for Several Modal Logics. advances in modal logic. pp. 309- 333 ,(2004)
Kai Brünnler, Atomic Cut Elimination for Classical Logic computer science logic. pp. 86- 97 ,(2003) , 10.1007/978-3-540-45220-1_9
Alessio Guglielmi, Lutz Straßburger, A Non-commutative Extension of MELL international conference on logic programming. pp. 231- 246 ,(2002) , 10.1007/3-540-36078-6_16
H. Schwichtenberg, A. S. Troelstra, Basic proof theory ,(1996)
Kai Brünnler, Alwen Fernanto Tiu, A Local System for Classical Logic Logic for Programming, Artificial Intelligence, and Reasoning. pp. 347- 361 ,(2001) , 10.1007/3-540-45653-8_24
Jacques Herbrand, Recherches sur la théorie de la démonstration Thèses françaises de l'entre-deux-guerres. ,vol. 110, pp. 1- 128 ,(1930)
Alessio Guglielmi, A system of interaction and structure ACM Transactions on Computational Logic. ,vol. 8, pp. 1- ,(2007) , 10.1145/1182613.1182614
Paola Bruscoli, A Purely Logical Account of Sequentiality in Proof Search international conference on logic programming. pp. 302- 316 ,(2002) , 10.1007/3-540-45619-8_21
Kai Brünnler, Locality for Classical Logic Notre Dame Journal of Formal Logic. ,vol. 47, pp. 557- 580 ,(2006) , 10.1305/NDJFL/1168352668
Lutz Straβburger, A Local System for Linear Logic international conference on logic programming. pp. 388- 402 ,(2002) , 10.1007/3-540-36078-6_26