Essential structure of proofs as a measure of complexity

DOI10.1007/S11787-020-00251-4MaRDI QIDQ2183713zbMATH OpenOpenAlexWikidataFDO

Authors Jaime Ramos, João Rasga, Cristina Sernadas

Publication date 27 May 2020

Published in Logica Universalis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11787-020-00251-4

zbMATH Keywords

description complexityschema calculusschema derivationuniform and non-uniform robustness

Mathematics Subject Classification ID

Classical first-order logic (03B10) Abstract deductive systems (03B22) Proof theory in general (including proof-theoretic semantics) (03F03) Complexity of proofs (03F20)

Review text

The article is well organized and written. Mainly, it shows that introducing the notions of \textit{schema calculus, schema derivation} and \textit{description complexity of a schema formula}, they were able to recognize that two distinct derivations of two distinct theorems can be the same in the sense that both are instances of the same schema derivation, so, intuitively both must have the same description complexity in an appropriate schema calculus. Besides, using these concepts they prove general robustness results relating to description complexity of a schema formula across Hilbert and Gentzen calculus. In page 212, inside the definition of \textit{schema calculus}, subpart \textit{proviso oracle map}, it will be appropriate to explicitly mention that \(\Lambda \subseteq A\).

Recommendations

• On meta complexity of propositional formulas and propositional proofs
• Proof complexity and textual cohesion
• On complexity of statements and meaningful complexity of an axiomatic theory
• scientific article; zbMATH DE number 937363
• scientific article; zbMATH DE number 3954903

Cites work

• Combinatorial foundations of information theory and the calculus of probabilities
• Hilbert's Twenty-Fourth Problem
• scientific article; zbMATH DE number 48365 (Why is no real title available?)
• scientific article; zbMATH DE number 481931 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 2212138 (Why is no real title available?)
• Kolmogorov and mathematical logic
• Modulated fibring and the collapsing problem
• Normal proofs, cut free derivations and structural rules
• On the idea of a general proof theory
• On the number of steps in proofs
• Preservation of admissible rules when combining logics
• Proof complexity of intuitionistic implicational formulas
• Some Results on the Length of Proofs
• Structural proof theory. With an appendix by Aarne Ranta
• The number of proof lines and the size of proofs in first order logic

Cited in

(3)

• Finding good proofs for description logic entailments using recursive quality measures
• scientific article; zbMATH DE number 176240 (Why is no real title available?)
• On complexity of statements and meaningful complexity of an axiomatic theory

Describes a project that uses

Uses Software

• Pesca

This page was built for publication: Essential structure of proofs as a measure of complexity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2183713)