Proof complexity (original) (raw)
Em ciência da computação, complexidade de prova é a medida da eficiência dos métodos de prova de teoremas automatizados que é baseado no tamanho das provas que produzem. Os métodos para provar por contradição na lógica proposicional são os mais analisados, Os dois principais problemas considerados na complexidade de prova são se um método de prova pode produzir uma prova polinomial para toda fórmula inconsistente, e se as provas produzidas por um método são sempre de tamanho semelhante a aquelas produzidas por outro método.
| Property | Value |
|---|---|
| dbo:abstract | En informatique théorique, la complexité des preuves ou complexité des démonstrations est le domaine qui étudie les ressources nécessaires pour prouver ou réfuter un énoncé mathématique. Le démarche classique du domaine est de fixer une sorte de preuve, puis de montrer des bornes sur la longueur des preuves pour certains énoncés. La sorte de preuve peut être d'origine logique, comme la déduction naturelle, le calcul des séquents, des systèmes basés sur la règle de résolution, ou plus combinatoire, comme l'algorithme DPLL et la méthode des plans sécants. Pour chacun il faut définir une notion de longueur pertinente. Le domaine est lié à la théorie de la complexité et aux assistants de preuve. Il a aussi de fortes relations avec les circuits booléens. (fr) In logic and theoretical computer science, and specifically proof theory and computational complexity theory, proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements. Research in proof complexity is predominantly concerned with proving proof-length lower and upper bounds in various propositional proof systems. For example, among the major challenges of proof complexity is showing that the Frege system, the usual propositional calculus, does not admit polynomial-size proofs of all tautologies. Here the size of the proof is simply the number of symbols in it, and a proof is said to be of polynomial size if it is polynomial in the size of the tautology it proves. Systematic study of proof complexity began with the work of Stephen Cook and (1979) who provided the basic definition of a propositional proof system from the perspective of computational complexity. Specifically Cook and Reckhow observed that proving proof size lower bounds on stronger and stronger propositional proof systems can be viewed as a step towards separating NP from coNP (and thus P from NP), since the existence of a propositional proof system that admits polynomial size proofs for all tautologies is equivalent to NP=coNP. Contemporary proof complexity research draws ideas and methods from many areas in computational complexity, algorithms and mathematics. Since many important algorithms and algorithmic techniques can be cast as proof search algorithms for certain proof systems, proving lower bounds on proof sizes in these systems implies run-time lower bounds on the corresponding algorithms. This connects proof complexity to more applied areas such as SAT solving. Mathematical logic can also serve as a framework to study propositional proof sizes. First-order theories and, in particular, weak fragments of Peano arithmetic, which come under the name of bounded arithmetic, serve as uniform versions of propositional proof systems and provide further background for interpreting short propositional proofs in terms of various levels of feasible reasoning. (en) Em ciência da computação, complexidade de prova é a medida da eficiência dos métodos de prova de teoremas automatizados que é baseado no tamanho das provas que produzem. Os métodos para provar por contradição na lógica proposicional são os mais analisados, Os dois principais problemas considerados na complexidade de prova são se um método de prova pode produzir uma prova polinomial para toda fórmula inconsistente, e se as provas produzidas por um método são sempre de tamanho semelhante a aquelas produzidas por outro método. (pt) |
| dbo:wikiPageExternalLink | http://list.math.cas.cz/listinfo/proof-complexity http://www.karlin.mff.cuni.cz/~krajicek/prfdraft.html http://www.cs.toronto.edu/~sacook/homepage/book https://www.cs.cmu.edu/afs/cs/project/jair/pub/volume21/dixon04a-html/node9.html http://www.karlin.mff.cuni.cz/~krajicek/ecm.pdf |
| dbo:wikiPageID | 2801284 (xsd:integer) |
| dbo:wikiPageLength | 31293 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1091328366 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Propositional_calculus dbr:Modal_logic dbr:Model_(logic) dbr:NE_(complexity) dbr:NP_(complexity) dbr:Algorithm dbc:Automated_theorem_proving dbr:Peano_arithmetic dbr:Resolution_(logic) dbr:Cutting-plane_method dbr:DPLL_algorithm dbr:Bulletin_of_the_European_Association_for_Theoretical_Computer_Science dbr:Intuitionistic_logic dbr:Propositional_proof_system dbr:Mathematical_logic dbr:Bounded_arithmetic dbr:Model-theoretic dbr:NC_(complexity) dbr:Conflict-driven_clause_learning dbr:Logic dbr:Stephen_Cook dbr:Communication_complexity dbr:Computational_complexity_theory dbr:CoNP dbr:Key_exchange dbr:P_(complexity) dbr:Theoretical_computer_science dbr:P/poly dbr:Alex_Wilkie dbr:E_(complexity) dbr:European_Congress_of_Mathematics dbr:Non-monotonic_logic dbr:Nullstellensatz dbr:Proof_theory dbr:Quasi-polynomial_time dbr:Jeff_Paris_(mathematician) dbr:AC0 dbc:Logic_in_computer_science dbc:Computational_complexity_theory dbr:Disjunctive_normal_form dbr:Circuit_complexity dbr:Frege_system dbr:Miklós_Ajtai dbr:Second-order_logic dbr:Sequent_calculus dbr:SAT_solver dbr:Exponential_time_hypothesis dbr:Complexity_classes dbr:Non-classical_logic dbr:Parameterized_complexity dbr:RSA_encryption dbr:First-order_theories dbr:Zermelo_Fraenkel_set_theory dbr:Robert_Reckhow |
| dbp:wikiPageUsesTemplate | dbt:ECCC dbt:Citation dbt:Main dbt:Reflist dbt:See_also |
| dcterms:subject | dbc:Automated_theorem_proving dbc:Logic_in_computer_science dbc:Computational_complexity_theory |
| gold:hypernym | dbr:Measure |
| rdf:type | owl:Thing dbo:Software |
| rdfs:comment | Em ciência da computação, complexidade de prova é a medida da eficiência dos métodos de prova de teoremas automatizados que é baseado no tamanho das provas que produzem. Os métodos para provar por contradição na lógica proposicional são os mais analisados, Os dois principais problemas considerados na complexidade de prova são se um método de prova pode produzir uma prova polinomial para toda fórmula inconsistente, e se as provas produzidas por um método são sempre de tamanho semelhante a aquelas produzidas por outro método. (pt) En informatique théorique, la complexité des preuves ou complexité des démonstrations est le domaine qui étudie les ressources nécessaires pour prouver ou réfuter un énoncé mathématique. Le démarche classique du domaine est de fixer une sorte de preuve, puis de montrer des bornes sur la longueur des preuves pour certains énoncés. La sorte de preuve peut être d'origine logique, comme la déduction naturelle, le calcul des séquents, des systèmes basés sur la règle de résolution, ou plus combinatoire, comme l'algorithme DPLL et la méthode des plans sécants. Pour chacun il faut définir une notion de longueur pertinente. (fr) In logic and theoretical computer science, and specifically proof theory and computational complexity theory, proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements. Research in proof complexity is predominantly concerned with proving proof-length lower and upper bounds in various propositional proof systems. For example, among the major challenges of proof complexity is showing that the Frege system, the usual propositional calculus, does not admit polynomial-size proofs of all tautologies. Here the size of the proof is simply the number of symbols in it, and a proof is said to be of polynomial size if it is polynomial in the size of the tautology it proves. (en) |
| rdfs:label | Complexité des preuves (fr) Proof complexity (en) Complexidade de prova (pt) |
| rdfs:seeAlso | dbr:SAT_solver |
| owl:sameAs | freebase:Proof complexity wikidata:Proof complexity dbpedia-fr:Proof complexity dbpedia-pt:Proof complexity https://global.dbpedia.org/id/4tSPx |
| prov:wasDerivedFrom | wikipedia-en:Proof_complexity?oldid=1091328366&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Proof_complexity |
| is dbo:knownFor of | dbr:Stephen_Cook__Stephen_Cook__1 |
| is dbo:wikiPageDisambiguates of | dbr:Proof |
| is dbo:wikiPageRedirects of | dbr:Proof_Complexity |
| is dbo:wikiPageWikiLink of | dbr:Proof_(truth) dbr:Richard_Zach dbr:DPLL_algorithm dbr:Propositional_proof_system dbr:Bounded_arithmetic dbr:Proof_Complexity dbr:MAXEkSAT dbr:Stephen_Cook dbr:Computational_complexity_theory dbr:Automated_theorem_proving dbr:Avi_Wigderson dbr:Admissible_rule dbr:Toniann_Pitassi dbr:Proof dbr:Proof_procedure dbr:Proof_theory dbr:Samuel_Buss dbr:Frege_system |
| is foaf:primaryTopic of | wikipedia-en:Proof_complexity |