Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae

Je\v{r}\'abek showed that cuts in classical propositional logic proofs in deep inference can be eliminated in quasipolynomial time. The proof is indirect and it relies on a result of Atserias, Galesi and Pudl\'ak about monotone sequent calculus and a correspondence between that system and...

書誌詳細
出版年:	Logical Methods in Computer Science
主要な著者:	Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, Michel Parigot
フォーマット:	論文
言語:	英語
出版事項:	Logical Methods in Computer Science e.V. 2016-05-01
主題:	computer science - computational complexity computer science - logic in computer science f.4.1 f.2.2
オンライン･アクセス:	https://lmcs.episciences.org/1637/pdf

類似資料

Normalisation Control in Deep Inference via Atomic Flows
著者:: Alessio Guglielmi, 等
出版事項: (2008-03-01)

The complexity of global cardinality constraints
著者:: Andrei A. Bulatov, 等
出版事項: (2010-10-01)

Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
著者:: Lars Kuhtz, 等
出版事項: (2012-10-01)

Absorbing Subalgebras, Cyclic Terms, and the Constraint Satisfaction Problem
著者:: Libor Barto, 等
出版事項: (2012-02-01)

Normalisation by Evaluation for Type Theory, in Type Theory
著者:: Thorsten Altenkirch, 等
出版事項: (2017-10-01)

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
著者:: Jose Espirito Santo, 等
出版事項: (2009-05-01)

Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic
著者:: Vincent Atassi, 等
出版事項: (2007-11-01)

Formalizing Randomized Matching Algorithms
著者:: Dai Tri Man Le, 等
出版事項: (2012-08-01)

The complexity of linear-time temporal logic over the class of ordinals
著者:: Stephane Demri, 等
出版事項: (2010-12-01)

A proof of strong normalisation using domain theory
著者:: Thierry Coquand, 等
出版事項: (2007-12-01)

The language of Stratified Sets is confluent and strongly normalising
著者:: Murdoch J. Gabbay
出版事項: (2018-05-01)

Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
著者:: Beniamino Accattoli, 等
出版事項: (2012-03-01)

Tree-width for first order formulae
著者:: Isolde Adler, 等
出版事項: (2012-03-01)

Infinitary Combinatory Reduction Systems: Normalising Reduction Strategies
著者:: Jeroen Ketema, 等
出版事項: (2010-02-01)

Polynomial Size Analysis of First-Order Shapely Functions
著者:: Olha Shkaravska, 等
出版事項: (2009-05-01)

A System of Interaction and Structure II: The Need for Deep Inference
著者:: Alwen Tiu
出版事項: (2006-04-01)

Width and size of regular resolution proofs
著者:: Alasdair Urquhart
出版事項: (2012-06-01)

Pseudo-finite hard instances for a student-teacher game with a Nisan-Wigderson generator
著者:: Jan Krajíček
出版事項: (2012-08-01)

On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
著者:: Rajeev Gore, 等
出版事項: (2011-05-01)

Guarded Second-Order Logic, Spanning Trees, and Network Flows
著者:: Achim Blumensath
出版事項: (2010-02-01)

Scalar and Vectorial mu-calculus with Atoms
著者:: Bartek Klin, 等
出版事項: (2019-10-01)

Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity
著者:: Dušan Knop, 等
出版事項: (2019-12-01)

Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy
著者:: Benjamin Bisping, 等
出版事項: (2022-08-01)

Coalgebraic trace semantics via forgetful logics
著者:: Bartek Klin, 等
出版事項: (2017-04-01)

Labelled transition systems as a Stone space
著者:: Michael Huth
出版事項: (2005-01-01)

Conway games, algebraically and coalgebraically
著者:: Furio Honsell, 等
出版事項: (2011-09-01)

On the meaning of logical completeness
著者:: Michele Basaldella, 等
出版事項: (2010-12-01)

On Berry's conjectures about the stable order in PCF
著者:: Fritz Müller
出版事項: (2012-10-01)

Randomisation and Derandomisation in Descriptive Complexity Theory
著者:: Kord Eickmeyer, 等
出版事項: (2011-09-01)

Dynamic Dependency Pairs for Algebraic Functional Systems
著者:: Cynthia Kop, 等
出版事項: (2012-06-01)

Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda
著者:: Jean-Philippe Bernardy, 等
出版事項: (2016-06-01)

Exhaustible sets in higher-type computation
著者:: Martin Escardo
出版事項: (2008-08-01)

Models of Type Theory Based on Moore Paths
著者:: Ian Orton, 等
出版事項: (2019-01-01)

Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)
著者:: Simon Castellan, 等
出版事項: (2017-11-01)

Consistency and Completeness of Rewriting in the Calculus of Constructions
著者:: Daria Walukiewicz-Chrzaszcz, 等
出版事項: (2008-09-01)

Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets
著者:: Paolo Baldan, 等
出版事項: (2008-10-01)

On the locality of arb-invariant first-order formulas with modulo counting quantifiers
著者:: Frederik Harwath, 等
出版事項: (2017-04-01)

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
著者:: Sanjit A. Seshia, 等
出版事項: (2005-12-01)

Efficient Open World Reasoning for Planning
著者:: Tamara Babaian, 等
出版事項: (2006-09-01)

Coherent and finiteness spaces
著者:: Pierre Hyvernat
出版事項: (2011-09-01)