CIRQUENT CALCULUS SYSTEM CL8S VERSUS CALCULUS OF STRUCTURES SYSTEM SKSG FOR PROPOSITIONAL LOGIC

被引：0

作者：

Xu, Wenyan ^{[1
]}

Liu, Sanyang ^{[1
]}

机构：

[1] Xidian Univ, Dept Math, Xian, Peoples R China

来源：

QUANTITATIVE LOGIC AND SOFT COMPUTING | 2012年 / 5卷

关键词：

Cirquent calculus; Calculus of structures; Deep inference; Proof complexity;

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Cirquent calculus and calculus of structures are two approaches to proof theory. Both of them apply deep inference which modifies objects at any level rather than only around the root as is the case in sequent calculus. In this paper we compare the proof complexity of the cirquent calculus system CL8S and the calculus of structures system SKSg at the classical propositional level, and show that CL8S polynomially simulates SKSg.

引用

页码：144 / 149

页数：6

共 12 条

[1] Brunnler Kai., 2004, DEEP INFERENCE SYMME
[2] On the Proof Complexity of Deep Inference
Bruscoli, Paola
Guglielmi, Alessio
[J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2009, 10 (02)
[3] Guglielmi A., 2001, LECT NOTES COMPUTER
[4] A system of interaction and structure
Guglielmi, Alessio
[J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2007, 8 (01)
[5] Japaridze G, 2003, ANN PURE APPL LOGIC, V123, P1, DOI [10.1016/S0168-0072(03)00023-X, 10.1016/s0168-0072(03)00023-X]
[6] Japaridze G., 2008, J LOG COMPUTA, V18, P6
[7] Japaridze G., 2006, INTERACTIVE COMPUTAT, P183
[8] Japaridze G, 2006, J LOGIC COMPUT, V16, P489, DOI [10.1093/logcom/exl005, 10.1093/logcom/ex1005]
[9] FROM FORMULAS TO CIRQUENTS IN COMPUTABILITY LOGIC
Japaridze, Giorgi
[J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2011, 7 (02)
[10] Japaridze G, 2009, LOGIC EPISTEMOL UNIT, V15, P249

← 1 2 →