On the compressibility of finite languages and formal proofs

DOI10.1016/j.ic.2017.09.001zbMath1390.68389OpenAlexW2751273904WikidataQ113872847 ScholiaQ113872847MaRDI QIDQ1706152

Stefan Hetzl, Sebastian Eberhard

Publication date: 21 March 2018

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2017.09.001

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Complexity of proofs (03F20)

Related Items (4)

On minimizing regular expressions without Kleene star ⋮ On the Herbrand content of LK ⋮ On the cover complexity of finite languages ⋮ Inductive theorem proving based on tree grammars

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algorithmic introduction of quantified cuts
• Approximation of grammar-based compression via recompression
• Rigid tree automata and applications
• Context-free complexity of finite languages
• The epsilon calculus and Herbrand complexity
• A \textit{really} simple approximation of smallest grammar
• On the form of witness terms
• A lower-bound for the number of productions required for a certain class of languages
• Proof theory. 2nd ed
• On the context-free production complexity of finite languages
• The number of proof lines and the size of proofs in first order logic
• Concise description of finite languages
• A note on a problem in the theory of grammatical complexity
• Complexity of resolution proofs and function introduction
• Application of Lempel-Ziv factorization to the approximation of grammar-based compression.
• Untersuchungen über das logische Schliessen. II
• A fully linear-time approximation algorithm for grammar-based compression
• Algorithmics on SLP-compressed strings: A survey
• Applying Tree Languages in Proof Theory
• Towards Algorithmic Cut-Introduction
• Introducing Quantified Cuts in Logic with Equality
• Twelve Problems in Proof Complexity
• The Smallest Grammar Problem
• Lower Bounds on Herbrand's Theorem
• Grammar-based codes: a new class of universal lossless source codes
• On the Complexity of Grammar-Based Compression over Fixed Alphabets
• Herbrand Confluence for First-Order Proofs with Π₂-Cuts
• Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars
• Automated Reasoning
• The macro model for data compression (Extended Abstract)
• Compressibility of Finite Languages by Grammars
• Minimal cover-automata for finite languages

This page was built for publication: On the compressibility of finite languages and formal proofs