Quantifier elimination (original) (raw)
Quantorenelimination bezeichnet in der Modelltheorie eine bestimmte Eigenschaft von Theorien: Man sagt, eine Theorie habe Quantorenelimination, wenn jede Formel innerhalb der Theorie zu einer Formel ohne Quantoren äquivalent ist. So ist beispielsweise in einem Körper (also etwa in den reellen Zahlen) die Formel , die besagt, dass ein multiplikatives inverses Element besitzt, äquivalent zu , also dazu, dass . In kommen keine Quantoren mehr vor. Lässt sich jede Formel in eine solche quantorenfreie Formel umformen, so besitzt die Theorie Quantorenelimination. In Theorien mit Quantorenelimination können also beliebige Formeln in quantorenfreie und damit einfachere Formeln umgeformt werden.
| Property | Value |
|---|---|
| dbo:abstract | Quantorenelimination bezeichnet in der Modelltheorie eine bestimmte Eigenschaft von Theorien: Man sagt, eine Theorie habe Quantorenelimination, wenn jede Formel innerhalb der Theorie zu einer Formel ohne Quantoren äquivalent ist. So ist beispielsweise in einem Körper (also etwa in den reellen Zahlen) die Formel , die besagt, dass ein multiplikatives inverses Element besitzt, äquivalent zu , also dazu, dass . In kommen keine Quantoren mehr vor. Lässt sich jede Formel in eine solche quantorenfreie Formel umformen, so besitzt die Theorie Quantorenelimination. In Theorien mit Quantorenelimination können also beliebige Formeln in quantorenfreie und damit einfachere Formeln umgeformt werden. (de) La eliminación de cuantificadores es un concepto de simplificación utilizado en lógica matemática, teoría de modelos, y teoría de la computación. Informalmente, una proposición cuantificada, por ejemplo " tal que " puede verse como una pregunta: "¿Cuándo hay un tal que ?",y la proposición sin cuantificadores puede verse como la respuesta a esa pregunta. Un criterio de clasificación de fórmulas es atendiendo a su cantidad de cuantificadores. Las fórmulas con menos cuantificadores anidados son más simples, siendo las fórmulas en las que no aparecen cuanficiadores las más sencillas.Una teoría lógica tiene eliminación de cuantificadores si para cada fórmula , existe otra fórmula sin cuantificadores que es equivalente a ella ( de ese teorema). (es) En logique mathématique, ou plus précisément en théorie des modèles, l'élimination des quantificateurs est l'action consistant à trouver une formule sans quantificateur équivalente à une formule donnée contenant éventuellement des quantificateurs dans la théorie considérée d'un certain langage. Ainsi, si l'on considère la théorie des corps réels clos, le langage de cette théorie est L={+,•,<,0,1} où +,• sont deux symboles de fonction d'arité 2, < est un symbole de relation binaire, et 0,1 sont deux symboles de constante, la L-formule ∃x (ax² + bx + c = 0) est équivalente à la L-formule dans la théorie, car dans cette théorie ax² + bx + c = 0 admet une racine si et seulement si a, b et c sont tous nuls, ou a est nul mais b est non nul, ou a non nul et est positif. (fr) Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement " such that " can be viewed as a question "When is there an such that ?", and the statement without quantifiers can be viewed as the answer to that question. One way of classifying formulas is by the amount of quantification. Formulas with less depth of quantifier alternation are thought of as being simpler, with the quantifier-free formulas as the simplest.A theory has quantifier elimination if for every formula , there exists another formula without quantifiers that is equivalent to it (modulo this theory). (en) Eliminação de quantificadores é um conceito de simplificação usado na lógica matemática, teoria dos modelos, e ciência da computação teórica. Um meio de classificar fórmulas é pelo número de quantificadores. Fórmulas com menos alternância entre os quantificadores são consideradas mais simples, sendo a fórmula livre de quantificadores a mais simples.Uma teoria possui eliminação de quantificadores se para cada fórmula , existe outra fórmula sem quantificadores que é logicamente equivalente a ela. (pt) Элиминация кванторов — получение по заданной логической формуле эквивалентной ей, не содержащей кванторов. Теории, допускающие элиминацию кванторов для любой формулы, представляют особый интерес, поскольку наличие алгоритма элиминации позволяет получить ряд содержательных результатов об этой теории. Процессы нахождения алгоритмов элиминации кванторов для различных теорий имеют общие черты, что позволяет говорить о них как о едином методе. Название метод элиминации кванторов ввёл в обиход Тарский в 1935 году, хотя впервые соображения такого рода были применены ещё в 1927 году. Метод элиминации кванторов применим только к теориям очень специального вида, кроме того, каждый раз, когда этот метод применяется к новой теории, приходится проводить все доказательства с самого начала, так как арсенал общих результатов весьма скуден. Однако, если его удаётся применить, этот метод оказывается чрезвычайно полезным, так как даёт исчерпывающую информацию о данной теории. Обычно он также приводит к регулярному способу, позволяющему решить, принадлежит ли некоторое высказывание данной теории или нет — иными словами, даёт доказательство разрешимости теории. (ru) 量詞消去是數理邏輯、模型論與計算機科學中的一類技巧。我們稱一個理論可消去量詞，若且唯若對每個公式皆存在另一個不帶量詞的公式，使得兩者在該理論中等價，即：。 量詞消去在模型論有多種刻劃；即使一個理論可消去量詞，也不保證存在一個相應的演算法。 一個理論的量詞消去演算法係將一個帶量詞的公式轉成一個等價但不帶量詞的公式。利用這個演算法，我們能將任一句子（不帶自由變量的公式）轉成一個不帶變量的句子，後者通常可藉簡單的計算判定。因此，量詞消去演算法的存在性蘊含該理論的可判定性。 (zh) |
| dbo:wikiPageExternalLink | https://www21.in.tum.de/~nipkow/pubs/ijcar08.pdf https://www.usna.edu/CS/qepcadweb/B/QE.html https://infoscience.epfl.ch/record/110222/files/KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable.pdf |
| dbo:wikiPageID | 2150441 (xsd:integer) |
| dbo:wikiPageLength | 10586 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1121508988 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Cambridge_University_Press dbr:Elimination_theory dbr:Model_theory dbr:Boolean_algebras dbr:Algebraically_closed_field dbr:Algorithm dbr:Relation_(mathematics) dbr:Cylindrical_algebraic_decomposition dbr:Decidability_(logic) dbr:Presburger_arithmetic dbr:Mathematical_logic dbr:Modulo_(jargon) dbr:Conjunction_elimination dbr:Simplification_(disambiguation) dbr:Complete_theory dbr:Fundamenta_Mathematicae dbr:Substructure_(mathematics) dbr:Theoretical_computer_science dbr:Countable dbr:Amalgamation_property dbr:Feferman-Vaught_theorem dbr:Nullstellensatz dbr:Differentially_closed_field dbr:Formal_language dbr:Fourier–Motzkin_elimination dbr:Logical_equivalence dbr:Free_variable dbr:Well-formed_formula dbr:Quantifier_(logic) dbr:Atom_(order_theory) dbr:Abelian_group dbr:Academic_Press dbc:Model_theory dbr:Term_algebra dbr:Discriminant dbr:Disjunctive_normal_form dbr:Real_closed_field dbr:Sentence_(mathematical_logic) dbr:Tarski–Seidenberg_theorem dbr:Literal_(mathematical_logic) dbr:Dense_linear_order dbr:Random_graph dbr:Springer-Verlag dbr:Ordered_group dbr:Queue_(mathematics) dbr:Quadratic_polynomial dbr:Model_complete dbr:Logical_theory |
| dbp:date | October 2020 (en) |
| dbp:reason | complete sentence needed (en) |
| dbp:wikiPageUsesTemplate | dbt:Cite_book dbt:Cite_conference dbt:Cite_journal dbt:Cite_web dbt:Clarify dbt:Cn dbt:Harvtxt dbt:Refbegin dbt:Refend dbt:Reflist dbt:Sfn dbt:Harvid |
| dct:subject | dbc:Model_theory |
| rdfs:comment | Quantorenelimination bezeichnet in der Modelltheorie eine bestimmte Eigenschaft von Theorien: Man sagt, eine Theorie habe Quantorenelimination, wenn jede Formel innerhalb der Theorie zu einer Formel ohne Quantoren äquivalent ist. So ist beispielsweise in einem Körper (also etwa in den reellen Zahlen) die Formel , die besagt, dass ein multiplikatives inverses Element besitzt, äquivalent zu , also dazu, dass . In kommen keine Quantoren mehr vor. Lässt sich jede Formel in eine solche quantorenfreie Formel umformen, so besitzt die Theorie Quantorenelimination. In Theorien mit Quantorenelimination können also beliebige Formeln in quantorenfreie und damit einfachere Formeln umgeformt werden. (de) Eliminação de quantificadores é um conceito de simplificação usado na lógica matemática, teoria dos modelos, e ciência da computação teórica. Um meio de classificar fórmulas é pelo número de quantificadores. Fórmulas com menos alternância entre os quantificadores são consideradas mais simples, sendo a fórmula livre de quantificadores a mais simples.Uma teoria possui eliminação de quantificadores se para cada fórmula , existe outra fórmula sem quantificadores que é logicamente equivalente a ela. (pt) 量詞消去是數理邏輯、模型論與計算機科學中的一類技巧。我們稱一個理論可消去量詞，若且唯若對每個公式皆存在另一個不帶量詞的公式，使得兩者在該理論中等價，即：。 量詞消去在模型論有多種刻劃；即使一個理論可消去量詞，也不保證存在一個相應的演算法。 一個理論的量詞消去演算法係將一個帶量詞的公式轉成一個等價但不帶量詞的公式。利用這個演算法，我們能將任一句子（不帶自由變量的公式）轉成一個不帶變量的句子，後者通常可藉簡單的計算判定。因此，量詞消去演算法的存在性蘊含該理論的可判定性。 (zh) La eliminación de cuantificadores es un concepto de simplificación utilizado en lógica matemática, teoría de modelos, y teoría de la computación. Informalmente, una proposición cuantificada, por ejemplo " tal que " puede verse como una pregunta: "¿Cuándo hay un tal que ?",y la proposición sin cuantificadores puede verse como la respuesta a esa pregunta. (es) Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement " such that " can be viewed as a question "When is there an such that ?", and the statement without quantifiers can be viewed as the answer to that question. (en) En logique mathématique, ou plus précisément en théorie des modèles, l'élimination des quantificateurs est l'action consistant à trouver une formule sans quantificateur équivalente à une formule donnée contenant éventuellement des quantificateurs dans la théorie considérée d'un certain langage. (fr) Элиминация кванторов — получение по заданной логической формуле эквивалентной ей, не содержащей кванторов. Теории, допускающие элиминацию кванторов для любой формулы, представляют особый интерес, поскольку наличие алгоритма элиминации позволяет получить ряд содержательных результатов об этой теории. (ru) |
| rdfs:label | Quantorenelimination (de) Eliminación de cuantificadores (es) Élimination des quantificateurs (fr) Quantifier elimination (en) Eliminação de quantificadores (pt) Элиминация кванторов (ru) 量詞消去 (zh) |
| owl:sameAs | freebase:Quantifier elimination wikidata:Quantifier elimination dbpedia-de:Quantifier elimination dbpedia-es:Quantifier elimination dbpedia-fa:Quantifier elimination dbpedia-fr:Quantifier elimination dbpedia-he:Quantifier elimination dbpedia-pt:Quantifier elimination dbpedia-ru:Quantifier elimination dbpedia-zh:Quantifier elimination https://global.dbpedia.org/id/nFj2 |
| prov:wasDerivedFrom | wikipedia-en:Quantifier_elimination?oldid=1121508988&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Quantifier_elimination |
| is dbo:wikiPageDisambiguates of | dbr:QE |
| is dbo:wikiPageRedirects of | dbr:Quantifier_Elimination dbr:Algorithms_for_quantifier_elimination dbr:Elimination_of_quantifiers |
| is dbo:wikiPageWikiLink of | dbr:Elimination_theory dbr:List_of_computer_algebra_systems dbr:List_of_first-order_theories dbr:Model_theory dbr:Algebraically_closed_field dbr:Cylindrical_algebraic_decomposition dbr:Decidability_(logic) dbr:Decidability_of_first-order_theories_of_the_real_numbers dbr:Definable_set dbr:Index_of_philosophy_articles_(I–Q) dbr:James_Renegar dbr:List_of_mathematical_logic_topics dbr:O-minimal_theory dbr:Tarski's_axioms dbr:Presburger_arithmetic dbr:Zariski_geometry dbr:Quantifier_Elimination dbr:Mathematical_logic dbr:George_E._Collins dbr:Angus_Macintyre dbr:Sturm's_theorem dbr:Computer_algebra_system dbr:Feferman–Vaught_theorem dbr:Time_complexity dbr:Wanda_Szmielew dbr:Alfred_Tarski dbr:Algebraic_geometry dbr:Amalgamation_property dbr:Differentially_closed_field dbr:QE dbr:Quantifier_(logic) dbr:2-EXPTIME dbr:Term_algebra dbr:Real_algebraic_geometry dbr:Algorithms_for_quantifier_elimination dbr:Cantor's_isomorphism_theorem dbr:Real_closed_field dbr:Satisfiability_modulo_theories dbr:Skolem_arithmetic dbr:Type_(model_theory) dbr:Tarski–Seidenberg_theorem dbr:Two-element_Boolean_algebra dbr:Existential_theory_of_the_reals dbr:Wilkie's_theorem dbr:P-adically_closed_field dbr:Theory_of_pure_equality dbr:Elimination_of_quantifiers |
| is foaf:primaryTopic of | wikipedia-en:Quantifier_elimination |