INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH

DOI10.1017/JSL.2021.75MaRDI QIDQ5082067zbMATH OpenOpenAlexWikidataFDO

Authors Jan Krajíček

Publication date 15 June 2022

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2104.04711

zbMATH Keywords

algorithmic informationproof searchpropositional proof systems

Mathematics Subject Classification ID

Complexity of proofs (03F20) Communication complexity, information complexity (68Q11) Algorithmic information theory (Kolmogorov complexity, etc.) (68Q30)

Recommendations

• A proof-search procedure for intuitionistic propositional logic
• scientific article; zbMATH DE number 1303443
• The information in intuitionistic logic
• The Complexity of Propositional Proofs
• The Complexity of Propositional Proofs
• scientific article; zbMATH DE number 1860672
• scientific article; zbMATH DE number 1156870
• scientific article; zbMATH DE number 1390270
• scientific article; zbMATH DE number 3313427
• Extracting Information from Logical Proofs

Cites work

• 2019 IEEE 60th Annual Symposium on Foundations of Computer Science (FOCS)
• A note on SAT algorithms and proof complexity
• Algorithmic information theory
• Automating resolution is NP-hard
• Consequences of the provability of NP ⊆ P/poly
• Diagonalization in proof complexity
• Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds
• scientific article; zbMATH DE number 5845490 (Why is no real title available?)
• scientific article; zbMATH DE number 3427210 (Why is no real title available?)
• scientific article; zbMATH DE number 3557241 (Why is no real title available?)
• scientific article; zbMATH DE number 610968 (Why is no real title available?)
• Implicit proofs
• Information-Theoretic Limitations of Formal Systems
• Logical basis for information theory and probability theory
• On Interpolation and Automatization for Frege Systems
• Proof Complexity
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• Randomness conservation inequalities; information and independence in mathematical theories
• Short propositional refutations for dense random 3CNF formulas
• Some consequences of cryptographical conjectures for \(S_2^1\) and EF
• The intractability of resolution
• The relative efficiency of propositional proof systems

Cited in

(7)

• Extracting Information from Logical Proofs
• scientific article; zbMATH DE number 1303443 (Why is no real title available?)
• ON THE EXISTENCE OF STRONG PROOF COMPLEXITY GENERATORS
• Information in propositional proofs and algorithmic proof search
• Quantum automating TC^0-Frege is LWE-hard
• A proof complexity conjecture and the incompleteness theorem
• Quantum automating \(\mathrm{TC}^0\)-Frege is LWE-hard

This page was built for publication: INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH

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