, Monotone simulations of non-monotone proofs, Journal of Computer and System Sciences, vol.65, issue.4, pp.626-638, 2002.
DOI : 10.1016/S0022-0000(02)00020-X
, A first order system with finite choice of premises First-Order Logic Revisited, Logische Philosophie On analytic inference rules in the calculus of structures, Logos Verlag, pp.59-74, 2004.
, Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae, Logical Methods in Computer Science, vol.12, issue.2, 2009.
DOI : 10.2168/LMCS-12(2:5)2016
URL : https://hal.archives-ouvertes.fr/inria-00441213
, On two forms of bureaucracy in derivations, Structures and Deduction, pp.69-80
, A Purely Logical Account of Sequentiality in Proof Search, Logic Programming, 18th International Conference, pp.302-316, 2002.
DOI : 10.1007/3-540-45619-8_21
, Atomic Cut Elimination for Classical Logic, Lecture Notes in Computer Science, vol.2803, pp.86-97, 2003.
DOI : 10.1007/978-3-540-45220-1_9
, Two Restrictions on Contraction, Logic Journal of IGPL, vol.11, issue.5, pp.525-529, 2003.
DOI : 10.1093/jigpal/11.5.525
, Deep Inference and Symmetry in Classical Proofs, Logos Verlag, 2004.
, Cut Elimination inside a Deep Inference System for Classical Predicate Logic, Studia Logica, vol.11, issue.1, pp.51-71, 2006.
DOI : 10.1007/s11225-006-6605-4
, Deep Inference and Its Normal Form of Derivations, Computability in Europe, pp.65-74, 2006.
DOI : 10.1007/978-3-642-66473-1
, Deep sequent systems for modal logic Advances in Modal Logic, pp.107-119, 2006.
, Locality for Classical Logic, Notre Dame Journal of Formal Logic, vol.47, issue.4, pp.557-580, 2006.
DOI : 10.1305/ndjfl/1168352668
, A Local System for Classical Logic, Lecture Notes in Artificial Intelligence, vol.2250, pp.347-361, 2001.
DOI : 10.1007/3-540-45653-8_24
, Polynomial size proofs of the propositional pigeonhole principle, Journal of Symbolic Logic, vol.52, issue.4, pp.916-927, 1987.
, Boolean Functions and Computation Models On the lengths of proofs in the propositional calculus (preliminary version) The relative efficiency of propositional proof systems, Proceedings of the 6th annual ACM Symposium on Theory of Computing, pp.135-14836, 1974.
, Structures for multiplicative cyclic linear logic: Deepness vs cyclicity, Lecture Notes in Computer Science, vol.3210, pp.130-144, 2004.
, Normalisation Control in Deep Inference via Atomic Flows, Logical Methods in Computer Science, vol.4, issue.1, pp.1-361, 1987.
DOI : 10.2168/LMCS-4(1:9)2008
, Non-commutativity and MELL in the Calculus of Structures, Lecture Notes in Computer Science, vol.2142, pp.54-68, 2001.
DOI : 10.1007/3-540-44802-0_5
, A Non-commutative Extension of MELL, Lecture Notes in Artificial Intelligence, vol.2514, pp.231-246, 2002.
DOI : 10.1007/3-540-36078-6_16
, A system of interaction and structure V: the exponentials and splitting, Mathematical Structures in Computer Science, vol.21, issue.03, 2009.
DOI : 10.1017/S096012951100003X
URL : https://hal.archives-ouvertes.fr/inria-00441254
, Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5, Journal of Logic and Computation, vol.17, issue.4, pp.767-794, 2007.
DOI : 10.1093/logcom/exm026
, Resolution in the calculus of structures, Alessio Guglielmi. Formalism B, 2003.
, The problem of bureaucracy and identity of proofs from the perspective of deep inference, Structures and Deduction, pp.53-68, 2005.
, On the proof complexity of deep inference?Conjecture. Prolog program, 2007.
, A system of interaction and structure, ACM Transactions on Computational Logic, vol.8, issue.1, pp.1-64, 2007.
DOI : 10.1145/1182613.1182614
URL : https://hal.archives-ouvertes.fr/inria-00441214
, The three dimensions of proofs, Annals of Pure and Applied Logic, vol.141, issue.1-2, pp.266-295, 2006.
DOI : 10.1016/j.apal.2005.12.012
URL : https://hal.archives-ouvertes.fr/hal-00092212
, Cirquent Calculus Deepened, Journal of Logic and Computation, vol.18, issue.6, pp.983-1028, 2008.
DOI : 10.1093/logcom/exn019
, Proof Complexity of the Cut-free Calculus of Structures, Journal of Logic and Computation, vol.19, issue.2, pp.323-339, 2009.
DOI : 10.1093/logcom/exn054
, Nondeterminism and Language Design in Deep Inference, 2006.
, Reducing Nondeterminism in the Calculus of Structures, Proceedings of the Eighth International Workshop on Rule Based Programming, pp.272-2861, 2006.
DOI : 10.1007/11916277_19
, Constructing free boolean categories http://www.lix.polytechnique.fr/~lutz/papers/FreeBool-long.pdf . [LS05b] François Lamarche and Lutz Straßburger. Naming proofs in classical propositional logicLS06] François Lamarche and Lutz Straßburger. From proof nets to the free *-autonomous category, Propositional proof systems 20th Annual IEEE Symposium on Logic in Computer Science Typed Lambda Calculi and Applications, pp.1063-1079, 1976.
, On Proof Nets for Multiplicative Linear Logic with Units
DOI : 10.1007/978-3-540-30124-0_14
, Bounds for proof-search and speed-up in the predicate calculus, Annals of Mathematical Logic, vol.15, issue.3, pp.225-287, 1978.
DOI : 10.1016/0003-4843(78)90011-6
, A Deep Inference System for the Modal Logic S5, Studia Logica, vol.6, issue.5, pp.199-214, 2007.
DOI : 10.1007/s11225-007-9028-y
, A local system for linear logic, Lecture Notes in Artificial Intelligence, vol.2514, pp.388-402, 2002.
, Linear Logic and Noncommutativity in the Calculus of Structures, 2003.
, MELL in the calculus of structures, Theoretical Computer Science, vol.309, issue.1-3, pp.213-285, 2003.
DOI : 10.1016/S0304-3975(03)00240-8
, A Local System for Intuitionistic Logic, Lecture Notes in Artificial Intelligence, vol.4246, pp.242-256, 2006.
DOI : 10.1007/11916277_17
, A System of Interaction and Structure II: The Need for Deep Inference, Logical Methods in Computer Science, vol.2, issue.2, pp.1-24, 1996.
DOI : 10.2168/LMCS-2(2:4)2006