Search results for "cut-elimination"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
95	Olivier Hermant	Semantic Cut Elimination in the Intuitionistic Sequent Calculus.	TLCA	2005	DBLP DOI BibTeX RDF	intuitionistic sequent calculus, cut admissibility, cut elimination property, semantic, Kripke Structure, deduction modulo
89	Kai Brünnler	Atomic Cut Elimination for classical Logic.	CSL	2003	DBLP DOI BibTeX RDF	atomic cut, sequent calculus, cut elimination, natural deduction, classical logic
85	Christian Urban	Strong Normalisation for a Gentzen-like Cut-Elimination Procedure.	TLCA	2001	DBLP DOI BibTeX RDF	Recursive Path Ordering, Cut-Elimination, Explicit Substitution, Classical Logic
83	Agata Ciabattoni, Kazushige Terui	Modular Cut-Elimination: Finding Proofs or Counterexamples.	LPAR	2006	DBLP DOI BibTeX RDF
79	Francisco Gutiérrez, Blas C. Ruiz	Expansion Postponement via Cut Elimination in Sequent Calculi for Pure Type Systems.	ICALP	2003	DBLP DOI BibTeX RDF	pure type systems, expansion postponement, Track: B, cut elimination, sequent calculi
75	Kentaro Kikuchi	Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus.	CiE	2007	DBLP DOI BibTeX RDF	?-calculus, Sequent calculus, Cut-elimination, Confluence, Explicit substitution
69	Kai Brünnler	Cut Elimination inside a Deep Inference System for Classical Predicate Logic.	Stud Logica	2006	DBLP DOI BibTeX RDF	cut elimination, first-order predicate logic, deep inference
68	Francesco Belardinelli, Peter Jipsen, Hiroakira Ono	Algebraic Aspects of Cut Elimination.	Stud Logica	2004	DBLP DOI BibTeX RDF	Algebraic Gentzen systems, finite model property, residuated lattices, cut elimination, substructural logics
67	José Espírito Santo	Revisiting the Correspondence between Cut Elimination and Normalisation.	ICALP	2000	DBLP DOI BibTeX RDF
62	Harry G. Mairson, Kazushige Terui	On the Computational Complexity of Cut-Elimination in Linear Logic.	ICTCS	2003	DBLP DOI BibTeX RDF
58	Hugo Herbelin, Gyesik Lee	Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus.	WoLLIC	2009	DBLP DOI BibTeX RDF	Intuitionistic Gentzen-style sequent calculus, completeness, cut-elimination, Kripke semantics
58	Guillaume Burel, Claude Kirchner	Cut Elimination in Deduction Modulo by Abstract Completion.	LFCS	2007	DBLP DOI BibTeX RDF	Knuth-Bendix completion, automated deduction and interactive theorem proving, proof ordering, abstract canonical system, cut elimination, deduction modulo
57	Clément Houtmann	Axiom Directed Focusing.	TYPES	2008	DBLP DOI BibTeX RDF	superdeduction, Proof theory, focusing, deduction modulo
57	Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr	Cut-Elimination: Experiments with CERES.	LPAR	2004	DBLP DOI BibTeX RDF
56	Dirk Pattinson, Lutz Schröder	Generic Modal Cut Elimination Applied to Conditional Logics.	TABLEAUX	2009	DBLP DOI BibTeX RDF
56	Gilles Dowek, Olivier Hermant	A Simple Proof That Super-Consistency Implies Cut Elimination.	RTA	2007	DBLP DOI BibTeX RDF
56	Philipp Gerhardy	Refined Complexity Analysis of Cut Elimination.	CSL	2003	DBLP DOI BibTeX RDF
56	Christian Urban, Gavin M. Bierman	Strong Normalisation of Cut-Elimination in Classical Logic.	TLCA	1999	DBLP DOI BibTeX RDF
55	Grigori Mints	Unwinding a Non-effective Cut Elimination Proof.	CSR	2006	DBLP DOI BibTeX RDF
53	Olivier Laurent 0001, Roberto Maieli	Cut Elimination for Monomial MALL Proof Nets.	LICS	2008	DBLP DOI BibTeX RDF	Linear Logic, Cut Elimination, Proof Net
53	Agata Ciabattoni, Kazushige Terui	Towards a Semantic Characterization of Cut-Elimination.	Stud Logica	2006	DBLP DOI BibTeX RDF	nonclassical logicss, phase semantics, sequent calculus, cut-elimination, substructural logics
53	Anna Zamansky, Arnon Avron	Cut-Elimination and Quantification in Canonical Systems.	Stud Logica	2006	DBLP DOI BibTeX RDF	canonical systems, proof theory, cut elimination, non-deterministic matrices
53	Grigori Mints	Cut Elimination for S4C: A Case Study.	Stud Logica	2006	DBLP DOI BibTeX RDF	Dynamic topological logic, cut elimination
53	Torben Braüner, Valeria de Paiva	A Formulation of Linear Logic Based on Dependency-Relations.	CSL	1997	DBLP DOI BibTeX RDF
52	Koji Nakazawa	An Isomorphism Between Cut-Elimination Procedure and Proof Reduction.	TLCA	2007	DBLP DOI BibTeX RDF
51	Arnon Avron, Anna Zamansky	Canonical Signed Calculi, Non-deterministic Matrices and Cut-Elimination.	LFCS	2009	DBLP DOI BibTeX RDF
51	Kentaro Kikuchi	On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus.	LPAR	2006	DBLP DOI BibTeX RDF
51	Ichiro Ogata	Cut Elimination for Classical Proofs as Continuation Passing Style Computation.	ASIAN	1998	DBLP DOI BibTeX RDF
50	Matthias Baaz, Agata Ciabattoni	A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic.	TABLEAUX	2002	DBLP DOI BibTeX RDF
50	Francisco Gutiérrez, Blas C. Ruiz	A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene.	LOPSTR	2002	DBLP DOI BibTeX RDF	lambda calculus with types, pure type systems, cut elimination, sequent calculi
48	Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr	Proof Transformation by CERES.	MKM	2006	DBLP DOI BibTeX RDF
45	Michele Pagani	The Cut-Elimination Theorem for Differential Nets with Promotion.	TLCA	2009	DBLP DOI BibTeX RDF
45	Kentaro Kikuchi, Stéphane Lengrand	Strong Normalisation of Cut-Elimination That Simulates beta-Reduction.	FoSSaCS	2008	DBLP DOI BibTeX RDF
45	Olivier Hermant, James Lipton	A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms.	CSL	2008	DBLP DOI BibTeX RDF
45	Chiyan Chen, Dengping Zhu, Hongwei Xi	Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell.	PADL	2004	DBLP DOI BibTeX RDF
45	James Laird	A Deconstruction of Non-deterministic Classical Cut Elimination.	TLCA	2001	DBLP DOI BibTeX RDF
42	Claudia Faggian	Classical Proofs via Basic Logic.	CSL	1997	DBLP DOI BibTeX RDF
41	Arnon Avron, Anna Zamansky	A Triple Correspondence in Canonical Calculi: Strong Cut-Elimination, Coherence, and Non-deterministic Semantics.	CSR	2008	DBLP DOI BibTeX RDF
41	Norihiro Kamide	Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic.	CLIMA	2008	DBLP DOI BibTeX RDF
41	Gilles Dowek	Confluence as a Cut Elimination Property.	RTA	2003	DBLP DOI BibTeX RDF
41	Birgit Elbl	Cut elimination for a calculus with context-dependent rules.	Arch. Math. Log.	2001	DBLP DOI BibTeX RDF	Mathematics Subject Classification (2000): 03F05, 03B60, 68N17, 68Q55
41	Matthias Baaz, Alexander Leitsch	Comparing the Complexity of Cut-Elimination Methods.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF
40	Roy Dyckhoff, Delia Kesner, Stéphane Lengrand	Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic.	IJCAR	2006	DBLP DOI BibTeX RDF
39	Arnold Beckmann	Resolution Refutations and Propositional Proofs with Height-Restrictions.	CSL	2002	DBLP DOI BibTeX RDF	Height of proofs, Length of proofs, Resolution refutation, Frege systems, Order induction principle, Cut introduction, MSC: Primary 03F20, Secondary 03F07, 68R99, Cut elimination, 68Q15, Bounded arithmetic, Propositional calculus
37	José Espírito Santo	The lambda-Calculus and the Unity of Structural Proof Theory.	Theory Comput. Syst.	2009	DBLP DOI BibTeX RDF
35	Mirjana Borisavljevic	A Connection Between Cut Elimination and Normalization.	Arch. Math. Log.	2006	DBLP DOI BibTeX RDF
34	Norihiro Kamide	Proof Systems Combining Classical and Paraconsistent Negations.	Stud Logica	2009	DBLP DOI BibTeX RDF	Paraconsistent negation, completeness, sequent calculus, cut-elimination
34	Agata Ciabattoni, Nikolaos Galatos, Kazushige Terui	From Axioms to Analytic Rules in Nonclassical Logics.	LICS	2008	DBLP DOI BibTeX RDF	nonclassical logics, hypersequent calculi, semantic cut-elimination, sequent calculi
34	Alessio Guglielmi	A system of interaction and structure.	ACM Trans. Comput. Log.	2007	DBLP DOI BibTeX RDF	mix rule, noncommutativity, pomset logic, symmetry, linear logic, cut elimination, self-duality, deep inference, Calculus of structures
34	Aleksandra Kislak-Malinowska	On the Logic of beta -pregroups.	Stud Logica	2007	DBLP DOI BibTeX RDF	?-pregroup, normalization theorem, cut elimination, Pregroup
34	Annie Foret	Pregroup Calculus as a Logic Functor.	WoLLIC	2007	DBLP DOI BibTeX RDF	Lambek Categorial Grammars, Logic Functor, Cut Elimination, Pregroups
34	Matthias Baaz, Rosalie Iemhoff	Gentzen Calculi for the Existence Predicate.	Stud Logica	2006	DBLP DOI BibTeX RDF	existence predicate, Gentzen calculus, truth-value logics, Gödel logics, Scott logics, cut-elimination, Intuitionistic logic, Kripke models, Skolemization
34	Henry Towsner	Epsilon substitution for transfinite induction.	Arch. Math. Log.	2005	DBLP DOI BibTeX RDF	Epsilon substitution, Cut elimination
34	Matthias Baaz, Rosalie Iemhoff	On Interpolation in Existence Logics.	LPAR	2005	DBLP DOI BibTeX RDF	existence predicate, Gentzen calculus, Beth definability, truth-value logics, Gödel logics, Scott logics, interpolation, cut-elimination, Intuitionistic logic, Kripke models, Skolemization
34	Stefano Baratella, Andrea Masini	An approach to infinitary temporal proof theory.	Arch. Math. Log.	2004	DBLP DOI BibTeX RDF	Modal logic, Proof theory, Sequent calculus, Cut elimination, Infinitary logic
32	Agata Ciabattoni, George Metcalfe	Density Elimination and Rational Completeness for First-Order Logics.	LFCS	2007	DBLP DOI BibTeX RDF
32	Matthias Baaz, Alexander Leitsch	CERES in Many-Valued Logics.	LPAR	2004	DBLP DOI BibTeX RDF
32	Alessio Guglielmi, Lutz Straßburger	Non-commutativity and MELL in the Calculus of Structures.	CSL	2001	DBLP DOI BibTeX RDF
32	Michel Parigot	Free Deduction: An Analysis of "Computations" in Classical Logic.	RCLP	1991	DBLP DOI BibTeX RDF
31	Rajeev Goré, Linda Postniece, Alwen Tiu	Taming Displayed Tense Logics Using Nested Sequents with Deep Inference.	TABLEAUX	2009	DBLP DOI BibTeX RDF
30	Mirjana Borisavljevic	Two measures for proving Gentzen's Hauptsatz without mix.	Arch. Math. Log.	2003	DBLP DOI BibTeX RDF
30	Grigori Mints	Proof Search Tree and Cut Elimination.	Pillars of Computer Science	2008	DBLP DOI BibTeX RDF
30	Christian Urban, Bozhi Zhu	Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof.	RTA	2008	DBLP DOI BibTeX RDF
30	Serenella Cerrito, Delia Kesner	Pattern Matching as Cut Elimination.	LICS	1999	DBLP DOI BibTeX RDF
30	Roberto Di Cosmo, Delia Kesner	Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract).	LICS	1997	DBLP DOI BibTeX RDF
30	Matthias Baaz, Alexander Leitsch	Fast Cut-Elimination by Projection.	CSL	1996	DBLP DOI BibTeX RDF
30	Ulf R. Schmerl	A Cut-Elimination Procedure Designed for Evaluating Proofs as Programs.	CSL	1991	DBLP DOI BibTeX RDF
29	Daniel Murfet, William Troiani	Elimination and cut-elimination in multiplicative linear logic.	CoRR	2022	DBLP DOI BibTeX RDF
29	Adam Prenosil	Cut Elimination, Identity Elimination, and Interpolation in Super-Belnap Logics.	Stud Logica	2017	DBLP DOI BibTeX RDF
29	Matthias Baaz, Alexander Leitsch	Cut-elimination and Redundancy-elimination by Resolution.	J. Symb. Comput.	2000	DBLP DOI BibTeX RDF
27	José Espírito Santo	Refocusing Generalised Normalisation.	CiE	2007	DBLP DOI BibTeX RDF	generalised elimination rules, multiarity, normalisation
26	Hidenori Kurokawa	Hypersequent Calculus for Intuitionistic Logic with Classical Atoms.	LFCS	2007	DBLP DOI BibTeX RDF
26	Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio	Higher-Order Termination: From Kruskal to Computability.	LPAR	2006	DBLP DOI BibTeX RDF
26	Richard Bonichon, Olivier Hermant	On Constructive Cut Admissibility in Deduction Modulo.	TYPES	2006	DBLP DOI BibTeX RDF
25	Agata Ciabattoni, George Metcalfe	Bounded Lukasiewicz Logics.	TABLEAUX	2003	DBLP DOI BibTeX RDF
23	Massimo Bartoletti, Roberto Zunino	A Calculus of Contracting Processes.	LICS	2010	DBLP DOI BibTeX RDF	circular assume-guarantee, concurrent constraints, contracts, cut elimination
23	James Brotherston, Cristiano Calcagno	Classical BI: a logic for reasoning about dualising resources.	POPL	2009	DBLP DOI BibTeX RDF	bunched implications, classical bi, display logic, semantics, completeness, cut-elimination, resource models
23	Carsten Schürmann 0001, Jeffrey Sarnat	Structural Logical Relations.	LICS	2008	DBLP DOI BibTeX RDF	Twelf, Normalization, Logical Frameworks, Cut-Elimination, Logical Relations
23	Dominic J. D. Hughes, Rob J. van Glabbeek	Proof nets for unit-free multiplicative-additive linear logic.	ACM Trans. Comput. Log.	2005	DBLP DOI BibTeX RDF	Linear logic, cut elimination, additives, proof nets
23	Agata Ciabattoni	A proof-theoretical investigation of global intuitionistic (fuzzy) logic.	Arch. Math. Log.	2005	DBLP DOI BibTeX RDF	Modal predicate logics, Hypersequent calculi, Globalization, Cut-elimination
23	Gilles Dowek, Thérèse Hardin, Claude Kirchner	Theorem Proving Modulo.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	sequent calculus modulo, resolution, rewriting, automated theorem proving, higher-order logic, cut elimination, narrowing, Skolemization, deduction modulo
22	Georg Moser, Richard Zach	The Epsilon Calculus and Herbrand Complexity.	Stud Logica	2006	DBLP DOI BibTeX RDF	Hilbert's ?-calculus, epsilon theorems, Herbrand's theorem, proof complexity
22	Klaus Mayr	Refinements and Extensions of Model Elimination.	LPAR	1993	DBLP DOI BibTeX RDF
21	Stefan Hetzl, Alexander Leitsch, Daniel Weller 0001, Bruno Woltzenlogel Paleo	A Clausal Approach to Proof Analysis in Second-Order Logic.	LFCS	2009	DBLP DOI BibTeX RDF
21	Ugo Dal Lago, Luca Roversi, Luca Vercelli	Taming Modal Impredicativity: Superlazy Reduction.	LFCS	2009	DBLP DOI BibTeX RDF	Linear logic, proof theory, implicit computational complexity
21	Atsushi Ohori	A proof theory for machine code.	ACM Trans. Program. Lang. Syst.	2007	DBLP DOI BibTeX RDF	Curry-Howard isomorphism
21	José Espírito Santo	Delayed Substitutions.	RTA	2007	DBLP DOI BibTeX RDF
21	Stefan Hetzl, Alexander Leitsch	Proof Transformations and Structural Invariance.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
21	Herman Geuvers, Iris Loeb	From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions.	MFCS	2006	DBLP DOI BibTeX RDF
21	Anna Zamansky, Arnon Avron	Canonical Gentzen-Type Calculi with (n, k)-ary Quantifiers.	IJCAR	2006	DBLP DOI BibTeX RDF
21	François Lamarche, Lutz Straßburger	Naming Proofs in Classical Propositional Logic.	TLCA	2005	DBLP DOI BibTeX RDF
21	Esfandiar Haghverdi, Philip J. Scott	Towards a Typed Geometry of Interaction.	CSL	2005	DBLP DOI BibTeX RDF
21	Michel Parigot	On Constructive Existence.	TYPES	2004	DBLP DOI BibTeX RDF
21	Sara Negri	A normalizing system of natural deduction for intuitionistic linear logic.	Arch. Math. Log.	2002	DBLP DOI BibTeX RDF
21	Alessio Guglielmi, Lutz Straßburger	A Non-commutative Extension of MELL.	LPAR	2002	DBLP DOI BibTeX RDF
21	Roberto Di Cosmo, Delia Kesner, Emmanuel Polonowski	Proof Nets and Explicit Substitutions.	FoSSaCS	2000	DBLP DOI BibTeX RDF
21	Wilfried Sieg, Stanley S. Wainer	Program Transformation and Proof Transformation.	CSL	1993	DBLP DOI BibTeX RDF
20	Linda Buisman, Rajeev Goré	A Cut-Free Sequent Calculus for Bi-intuitionistic Logic.	TABLEAUX	2007	DBLP DOI BibTeX RDF
20	Matthias Baaz, George Metcalfe	Proof Theory for First Order Lukasiewicz Logic.	TABLEAUX	2007	DBLP DOI BibTeX RDF
20	Dale Miller 0001, Alexis Saurin	From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic.	CSL	2007	DBLP DOI BibTeX RDF