A focused approach to combining logics

Annals of Pure and Applied Logic - Tập 162 - Trang 679-697 - 2011
Chuck Liang1, Dale Miller2
1Department of Computer Science, Hofstra University, Hempstead, NY 11550, USA
2INRIA Saclay–Île-de-France and LIX/Ecole Polytechnique, 91128 Palaiseau, France

Tài liệu tham khảo

Andreoli, 1992, Logic programming with focusing proofs in linear logic, J. Logic Comput., 2, 297, 10.1093/logcom/2.3.297 D. Baelde, A linear approach to the proof-theory of least and greatest fixed points, Ph.D. Thesis, Ecole Polytechnique, Dec. 2008. Baelde, 2007, Least and greatest fixed points in linear logic, vol. 4790, 92 K. Chaudhuri, The focused inverse method for linear logic, Ph.D. Thesis, Carnegie Mellon University, technical report CMU-CS-06-162, Dec. 2006. Chaudhuri, 2008, Canonical sequent proofs via multi-focusing, vol. 273, 383 Danos, 1997, A new deconstructive logic: linear logic, J. Symbolic Logic, 62, 755, 10.2307/2275572 Dyckhoff, 2006, LJQ: a strongly focused calculus for intuitionistic logic, vol. 3988, 173 Gentzen, 1969, Investigations into logical deductions, 68 Girard, 1987, Linear logic, Theoret. Comput. Sci., 50, 1, 10.1016/0304-3975(87)90045-4 Girard, 1991, A new constructive logic: classical logic, Math. Structures Comput. Sci., 1, 255, 10.1017/S0960129500001328 Girard, 1993, On the unity of logic, Ann. Pure Appl. Logic, 59, 201, 10.1016/0168-0072(93)90093-S H. Herbelin, Séquents qu’on calcule: de l’interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes, Ph.D. Thesis, Université Paris 7, 1995. Jagadeesan, 2005, Testing concurrent systems: An interpretation of intuitionistic logic, vol. 3821, 517 O. Laurent, Etude de la polarisation en logique, Thèse de doctorat, Université Aix-Marseille II, Mar. 2002. Laurent, 2005, Polarized and focalized linear and classical proofs, Ann. Pure Appl. Logic, 134, 217, 10.1016/j.apal.2004.11.002 Liang, 2007, Focusing and polarization in intuitionistic logic, vol. 4646, 451 C. Liang, D. Miller, A unified sequent calculus for focused proofs, in: LICS: 24th Symp. on Logic in Computer Science, 2009, pp. 355–364. Liang, 2009, Focusing and polarization in linear, intuitionistic, and classical logics, Theoret. Comput. Sci., 410, 4747, 10.1016/j.tcs.2009.07.041 Miller, 1991, Uniform proofs as a foundation for logic programming, Ann. Pure Appl. Logic, 51, 125, 10.1016/0168-0072(91)90068-W Miller, 2007, Incorporating tables into proofs, vol. 4646, 466