Search results for "cut-elimination"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
16	Philipp Gerhardy, Ulrich Kohlenbach	Extracting Herbrand disjunctions by functional interpretation.	Arch. Math. Log.	2005	DBLP DOI BibTeX RDF	Herbrand’s theorem, functional interpretation
16	Chuck C. Liang, Dale Miller 0001	A Unified Sequent Calculus for Focused Proofs.	LICS	2009	DBLP DOI BibTeX RDF
16	Kai Brünnler, Lutz Straßburger	Modular Sequent Systems for Modal Logic.	TABLEAUX	2009	DBLP DOI BibTeX RDF
16	Guillaume Munch-Maccagnoni	Focalisation and Classical Realisability.	CSL	2009	DBLP DOI BibTeX RDF
16	Kaustuv Chaudhuri	Focusing Strategies in the Sequent Calculus of Synthetic Connectives.	LPAR	2008	DBLP DOI BibTeX RDF
16	David Baelde, Dale Miller 0001	Least and Greatest Fixed Points in Linear Logic.	LPAR	2007	DBLP DOI BibTeX RDF
16	José Espírito Santo	Completing Herbelin's Programme.	TLCA	2007	DBLP DOI BibTeX RDF
16	Raul Hakli, Sara Negri	Proof Theory for Distributed Knowledge.	CLIMA	2007	DBLP DOI BibTeX RDF
16	Norihiro Kamide	Phase Semantics and Petri Net Interpretation for Resource-Sensitive Strong Negation.	J. Log. Lang. Inf.	2006	DBLP DOI BibTeX RDF	electric circuit, linear logic with strong negation, Petri net with inhibitor arc, phase semantics, medical diagnosis
16	Sándor Jenei, Franco Montagna	Rényi-Ulam Game Semantics for Product Logic and for the Logic of Cancellative Hoops.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
16	Kazushige Terui	Proof Nets and Boolean Circuits.	LICS	2004	DBLP DOI BibTeX RDF
16	Raphaël Montelatici	Polarized Proof Nets with Cycles and Fixpoints Semantics.	TLCA	2003	DBLP DOI BibTeX RDF
16	José Espírito Santo	An Isomorphism between a Fragment of Sequent Calculus and an Extension of Natural Deduction.	LPAR	2002	DBLP DOI BibTeX RDF
16	Luigi Di Lascio	Hilbertian systems, analytic fuzzy tableaux and cut rule elimination in rational pavelka logic.	SEKE	2002	DBLP DOI BibTeX RDF	cut rule, fuzzy prepositional logic, galois relation, pavelka semantics, completeness, soundness, MV-algebra, tableaux
16	Harry G. Mairson, Xavier Rival	Proofnets and Context Semantics for the Additives.	CSL	2002	DBLP DOI BibTeX RDF
16	Jan von Plato	A proof of Gentzen's Hauptsatz without multicut.	Arch. Math. Log.	2001	DBLP DOI BibTeX RDF
16	Pierre-Louis Curien	Abstract Machines, Control, and Sequents.	APPSEM	2000	DBLP DOI BibTeX RDF
16	Siani Baker, Andrew Ireland, Alan Smaill	On the Use of the Constructive Omega-Rule within Automated Deduction.	LPAR	1992	DBLP DOI BibTeX RDF
16	Regimantas Pliuskevicius	Investigation of Finitary Calculus for a Discrete Linear Time Logic by means of Infinitary Calculus.	Baltic Computer Science	1991	DBLP DOI BibTeX RDF
11	Giuseppe Castagna, Nils Gesbert, Luca Padovani	A theory of contracts for Web services.	ACM Trans. Program. Lang. Syst.	2009	DBLP DOI BibTeX RDF	explicit coercions, must testing, Web services, contracts, subtyping, type theory, ccs, concurrency theory
11	Katsuhiko Sano	Sound and Complete Tree-Sequent Calculus for Inquisitive Logic.	WoLLIC	2009	DBLP DOI BibTeX RDF
11	Linda Postniece	Deep Inference in Bi-intuitionistic Logic.	WoLLIC	2009	DBLP DOI BibTeX RDF
11	Lionel Vaux	Differential Linear Logic and Polarization.	TLCA	2009	DBLP DOI BibTeX RDF
11	Lutz Straßburger	Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic.	TLCA	2009	DBLP DOI BibTeX RDF
11	Marco Gaboardi, Luca Roversi, Luca Vercelli	A By-Level Analysis of Multiplicative Exponential Linear Logic.	MFCS	2009	DBLP DOI BibTeX RDF
11	Sean McLaughlin, Frank Pfenning	Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method.	CADE	2009	DBLP DOI BibTeX RDF
11	Arnon Avron, Ori Lahav 0001	Canonical Constructive Systems.	TABLEAUX	2009	DBLP DOI BibTeX RDF
11	George Metcalfe, Nicola Olivetti	Proof Systems for a Gödel Modal Logic.	TABLEAUX	2009	DBLP DOI BibTeX RDF
11	Max I. Kanovich	Light Linear Logic with Controlled Weakening.	LFCS	2009	DBLP DOI BibTeX RDF
11	Alwen Tiu, Rajeev Goré	A Proof Theoretic Analysis of Intruder Theories.	RTA	2009	DBLP DOI BibTeX RDF	AC convergent theories, intruder deduction, security protocols, sequent calculus
11	Agata Ciabattoni, Lutz Straßburger, Kazushige Terui	Expanding the Realm of Systematic Proof Theory.	CSL	2009	DBLP DOI BibTeX RDF
11	Fernando Ferreira 0001, Gilda Ferreira	Harrington's conservation theorem redone.	Arch. Math. Log.	2008	DBLP DOI BibTeX RDF	Mathematics Subject Classification (2000) 03F35, 03F07, 03F05
11	Henry DeYoung, Deepak Garg 0001, Frank Pfenning	An Authorization Logic With Explicit Time.	CSF	2008	DBLP DOI BibTeX RDF	Explicit Time, Hybrid Logic, Authorization Logic
11	Giuseppe Castagna, Nils Gesbert, Luca Padovani	A theory of contracts for web services.	POPL	2008	DBLP DOI BibTeX RDF	explicit coercions, must testing, web services, contracts, subtyping, type theory, CCS, concurrency theory
11	Alexandre Rademaker, Edward Hermann Haeusler	Toward Short and Structural -Reasoning Explanations: A Sequent Calculus Approach.	SBIA	2008	DBLP DOI BibTeX RDF	description logics, proof theory, sequent calculus
11	Alexis Saurin	Towards Ludics Programming: Interactive Proof Search.	ICLP	2008	DBLP DOI BibTeX RDF	Ludics, Proof Normalization, Interaction, Logic Programming, Game Semantics, Proof Search
11	Norihiro Kamide	Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials.	JELIA	2008	DBLP DOI BibTeX RDF
11	J. G. Cederquist, Ricardo Corin, M. A. C. Dekker, Sandro Etalle, J. I. den Hartog, Gabriele Lenzini	Audit-based compliance control.	Int. J. Inf. Sec.	2007	DBLP DOI BibTeX RDF	Privacy, Access control, Policy, Audit
11	Wojciech Buszkowski	Type Logics and Pregroups.	Stud Logica	2007	DBLP DOI BibTeX RDF	bilinear algebra, substructural logics, pregroup, Lambek calculus
11	Gabriele Pulcini	Permutative Additives and Exponentials.	LPAR	2007	DBLP DOI BibTeX RDF
11	Christophe Fouqueré	A Logical Calculus for Modelling Interferences.	ICTAC	2007	DBLP DOI BibTeX RDF
11	Paul Brauner, Clément Houtmann, Claude Kirchner	Principles of Superdeduction.	LICS	2007	DBLP DOI BibTeX RDF
11	Ping Hou, Johan Wittocx, Marc Denecker	A Deductive System for PC(ID).	LPNMR	2007	DBLP DOI BibTeX RDF
11	Arnon Avron, Anna Zamansky	Generalized Non-deterministic Matrices and (n, k)-ary Quantifiers.	LFCS	2007	DBLP DOI BibTeX RDF
11	Samson Abramsky	Full Completeness: Interactive and Geometric Characterizations of the Space of Proofs (Abstract).	CSL	2007	DBLP DOI BibTeX RDF
11	Georg Struth	Tableaux for Lattices.	AMAST	2006	DBLP DOI BibTeX RDF
11	Deepak Garg 0001, Frank Pfenning	Non-Interference in Constructive Authorization Logic.	CSFW	2006	DBLP DOI BibTeX RDF
11	Limin Jia 0001, David Walker 0001	ILC: A Foundation for Automated Reasoning About Pointer Programs.	ESOP	2006	DBLP DOI BibTeX RDF
11	Murdoch Gabbay, Aad Mathijssen	One-and-a-halfth-order logic.	PPDP	2006	DBLP DOI BibTeX RDF	?-conversion, Fraenkel-Mostowski techniques, meta-variables, nominal terms, first-order logic, higher-order logic
11	Deepak Garg 0001, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter	A Linear Logic of Authorization and Knowledge.	ESORICS	2006	DBLP DOI BibTeX RDF
11	Stéphane Lengrand, Roy Dyckhoff, James McKinna	A Sequent Calculus for Type Theory.	CSL	2006	DBLP DOI BibTeX RDF
11	Mauro Ferrari 0002, Camillo Fiorentini, Guido Fiorino	On the complexity of the disjunction property in intuitionistic and modal logics.	ACM Trans. Comput. Log.	2005	DBLP DOI BibTeX RDF	feasible interpolation, proof-length, modal logic, Intuitionistic logic
11	Dale Miller 0001, Alwen Tiu	A proof theory for generic judgments.	ACM Trans. Comput. Log.	2005	DBLP DOI BibTeX RDF	?-tree syntax, ?-quantifier, generic judgments, reasoning about operational semantics, higher-order abstract syntax, Proof search
11	Maciej Farulewski	On Finite Models of the Lambek Calculus.	Stud Logica	2005	DBLP DOI BibTeX RDF	finite model property, substructural logics, Lambek Calculus
11	Norihiro Kamide	Gentzen-Type Methods for Bilattice Negation.	Stud Logica	2005	DBLP DOI BibTeX RDF	Bilattice negation, completeness, sequent calculus, substructural logic, strong negation
11	Elaine Pimentel, Dale Miller 0001	On the Specification of Sequent Systems.	LPAR	2005	DBLP DOI BibTeX RDF
11	James Cheney	A Simpler Proof Theory for Nominal Logic.	FoSSaCS	2005	DBLP DOI BibTeX RDF
11	Marcelo da Silva Corrêa, Edward Hermann Haeusler	On the Selective Lambek Calculus.	LACL	2005	DBLP DOI BibTeX RDF
11	Alwen Fernanto Tiu	Model Checking for pi-Calculus Using Proof Search.	CONCUR	2005	DBLP DOI BibTeX RDF
11	Jean-Marc Andreoli, Gabriele Pulcini, Paul Ruet	Permutative Logic.	CSL	2005	DBLP DOI BibTeX RDF
11	Murdoch Gabbay, James Cheney	A Sequent Calculus for Nominal Logic.	LICS	2004	DBLP DOI BibTeX RDF
11	Kentaro Kikuchi	A Direct Proof of Strong Normalization for an Extended Herbelin?s Calculus.	FLOPS	2004	DBLP DOI BibTeX RDF
11	Herman Geuvers, Rob Nederpelt	Rewriting for Fitch Style Natural Deductions.	RTA	2004	DBLP DOI BibTeX RDF
11	Lutz Straßburger, François Lamarche	On Proof Nets for Multiplicative Linear Logic with Units.	CSL	2004	DBLP DOI BibTeX RDF
11	Pietro Di Gianantonio	Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity.	CSL	2004	DBLP DOI BibTeX RDF	cyclic linear logic, linear logic, proof theory, Lambek calculus, calculus of structures
11	Paola Bruscoli, Alessio Guglielmi	On Structuring Proof Search for First Order Linear Logic.	LPAR	2003	DBLP DOI BibTeX RDF
11	Dale Miller 0001, Alwen Fernanto Tiu	A Proof Theory for Generic Judgments: An extended abstract.	LICS	2003	DBLP DOI BibTeX RDF	reasoning about operational semantics, generic judgments, higher-order abstract syntax, proof search
11	Pierre Corbineau	First-Order Reasoning in the Calculus of Inductive Constructions.	TYPES	2003	DBLP DOI BibTeX RDF
11	Alberto Momigliano, Alwen Fernanto Tiu	Induction and Co-induction in Sequent Calculus.	TYPES	2003	DBLP DOI BibTeX RDF
11	Olivier Brunet	A Labelled Sequent-Calculus for Observation Logic.	TABLEAUX	2003	DBLP DOI BibTeX RDF
11	Toshiyasu Arai	Epsilon substitution method for theories of jump hierarchies.	Arch. Math. Log.	2002	DBLP DOI BibTeX RDF
11	Dale Miller 0001, Elaine Pimentel	Using Linear Logic to Reason about Sequent Systems.	TABLEAUX	2002	DBLP DOI BibTeX RDF
11	Claudia Faggian	Travelling on Designs.	CSL	2002	DBLP DOI BibTeX RDF
11	Ichiro Ogata	A Proof Theoretical Account of Continuation Passing Style.	CSL	2002	DBLP DOI BibTeX RDF	Classical Natural Deduction, LKQ, classical proof theory, Classical Logic, CPS-translation, Call-By-Value
11	Maribel Fernández, Ian Mackie	Call-by-Value lambda-Graph Rewriting Without Rewriting.	ICGT	2002	DBLP DOI BibTeX RDF
11	Kai Brünnler, Alwen Fernanto Tiu	A Local System for Classical Logic.	LPAR	2001	DBLP DOI BibTeX RDF
11	Arnon Avron, Iddo Lev	Canonical Propositional Gentzen-Type Systems.	IJCAR	2001	DBLP DOI BibTeX RDF
11	Jean-Yves Marion	Actual Arithmetic and Feasibility.	CSL	2001	DBLP DOI BibTeX RDF
11	Julia L. Lawall, Harry G. Mairson	Sharing Continuations: Proofnets for Languages with Explicit Control.	ESOP	2000	DBLP DOI BibTeX RDF
11	Andrzej S. Murawski, C.-H. Luke Ong	Discreet Games, Light Affine Logic and PTIME Computation.	CSL	2000	DBLP DOI BibTeX RDF	PTIME, Complexity, Linear Logic, Game Semantics
11	Matthias Baaz, Richard Zach	Hypersequent and the Proof Theory of Intuitionistic Fuzzy Logic.	CSL	2000	DBLP DOI BibTeX RDF
11	Sara Negri	Sequent calculus proof theory of intuitionistic apartness and order relations.	Arch. Math. Log.	1999	DBLP DOI BibTeX RDF
11	Atsushi Ohori	A Curry-Howard Isomorphism for Compilation and Program Execution.	TLCA	1999	DBLP DOI BibTeX RDF
11	Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller, Helmut Veith	On the Undecidability of some Sub-Classical First-Order Logics.	FSTTCS	1999	DBLP DOI BibTeX RDF
11	Masahiro Hamano, Mitsuhiro Okada	A direct independence proof of Buchholz's Hydra Game on finite labeled trees.	Arch. Math. Log.	1998	DBLP DOI BibTeX RDF	Mathematics Subject Classification: 03F03, 03F35, 03F05
11	Gianluigi Bellin, Arnaud Fleury	Planar and braided proof-nets for multiplicative linear logic with mix.	Arch. Math. Log.	1998	DBLP DOI BibTeX RDF
11	Martin Wirsing, John N. Crossley, Hannes Peterreins	Proof Normalization of Structured Algebraic Specifications Is Convergent.	WADT	1998	DBLP DOI BibTeX RDF
11	Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller, Helmut Veith	Proof Theory of Fuzzy Logics: Urquhart's C and Related Logics.	MFCS	1998	DBLP DOI BibTeX RDF
11	Jeremy E. Dawson, Rajeev Goré	A Mechanised Proof System for Relation Algebra using Display Logic.	JELIA	1998	DBLP DOI BibTeX RDF
11	Jerzy Tiuryn	A Sequent Calculus for Subtyping Polymorphic Types.	MFCS	1996	DBLP DOI BibTeX RDF
11	Stefano Guerrini, Simone Martini 0001, Andrea Masini	Coherence for Sharing Proof Nets.	RTA	1996	DBLP DOI BibTeX RDF
11	Dale Miller 0001	Specifications Using Multiple-Conclusion Logic Programs.	PLILP	1994	DBLP DOI BibTeX RDF
11	Matt Fairtlough, Michael Mendler	An Intuitionistic Modal Logic with Applications to the Formal Verification of Hardware.	CSL	1994	DBLP DOI BibTeX RDF
11	David A. Basin, Seán Matthews	A Conservative Extension of First-order Logic and Its Application to Theorem Proving.	FSTTCS	1993	DBLP DOI BibTeX RDF
11	Daniel Lehmann 0001	Plausibility Logic.	CSL	1991	DBLP DOI BibTeX RDF
11	John V. Tucker, Stanley S. Wainer, Jeffery I. Zucker	Provable Computable Functions on Abstract Data Types.	ICALP	1990	DBLP DOI BibTeX RDF