Resolution (logic) (original) (raw)
Die Resolution ist ein Verfahren der formalen Logik, um eine logische Formel auf Gültigkeit zu testen. Das Resolutionsverfahren, auch Resolutionskalkül genannt, ist ein Widerlegungsverfahren: Statt direkt die Allgemeingültigkeit einer Formel zu zeigen, leitet es einen logischen Widerspruch aus deren Verneinung ab. Diese Herleitung geschieht mittels eines Algorithmus auf rein formalem Weg und kann deshalb von einem Computerprogramm durchgeführt werden. Die Resolution ist eine der bekanntesten Techniken des Maschinengestützten Beweisens.
| Property | Value |
|---|---|
| dbo:abstract | Rezoluce je v logice metoda automatického dokazování tvrzení zavedená Alanem Robinsonem v roce 1965. Pro výrokovou logiku má tvar , kde a jsou disjunkce literálů. se nazývá resolventou. V predikátové logice má rezoluce podobu , kde je substituce unifikující a . V obecnosti je možné a obecně nutné vybrat a unifikovat víc pozitivních literálů v jedné a víc negovaných literálů ve druhé klauzuli. Rezoluce je odvozovací pravidlo a může být použito pro libovolné formule A a B ve výrokové i predikátové logice. Při dokazování a problému splnitelnosti (SAT) se obecné formule převedou na klauzule a pak stačí rezoluce jako jediné odvozovací pravidlo. Resolventa není ekvivalentní původní konjunkci klauzulí, ale platí , a proto pokud je resolventa nesplnitelná, je nesplnitelná i původní konjunkce klauzulí.Rezoluce tedy dokazuje tvrzení sporem. Chceme-li dokázat , přidáme do množiny formulí . Pokud rezoluce dojde ke sporu (tj. k prázdné klauzuli, jinými slovy ke klauzuli s prázdnou množinou literálů), je uvažovaná množina formulí nesplnitelná a podle Herbrandovy věty tím je tvrzení dokázáno. V logice s rovností se k rezoluci přidává odvozovací pravidlo paramodulace. Na principu rezoluce jsou založeny logické programovací jazyky, například Prolog, který používá a Hornovy klauzule. (cs) Die Resolution ist ein Verfahren der formalen Logik, um eine logische Formel auf Gültigkeit zu testen. Das Resolutionsverfahren, auch Resolutionskalkül genannt, ist ein Widerlegungsverfahren: Statt direkt die Allgemeingültigkeit einer Formel zu zeigen, leitet es einen logischen Widerspruch aus deren Verneinung ab. Diese Herleitung geschieht mittels eines Algorithmus auf rein formalem Weg und kann deshalb von einem Computerprogramm durchgeführt werden. Die Resolution ist eine der bekanntesten Techniken des Maschinengestützten Beweisens. (de) En logique mathématique, la règle de résolution ou principe de résolution de Robinson est une règle d'inférence logique qui généralise le modus ponens. Cette règle est principalement utilisée dans les systèmes de preuve automatiques, elle est à la base du langage de programmation logique Prolog. (fr) En Lógica Resolución es una regla de inferencia utilizada sobre cierto tipo de proposiciones lógicas y es especialmente utilizada para los demostradores automatizados de teoremas. Utilizando resolución se puede construir un demostrador que sea completo (por contradicción) y correcto (en inglés refutational complete and sound) para la lógica proposicional y de primer orden supuesto que un conjunto de proposiciones son insatisfacibles. Por otro lado si el conjunto de proposiciones de hecho es satisfacible, puede o no terminar en una cantidad finita de pasos una demostración por resolución, generalmente lo que sucede es que se asigna un tiempo límite para hallar si un conjunto es insatisfacible o no. (es) In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the (complement of the) Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem. The resolution rule can be traced back to Davis and Putnam (1960); however, their algorithm required trying all ground instances of the given formula. This source of combinatorial explosion was eliminated in 1965 by John Alan Robinson's syntactical unification algorithm, which allowed one to instantiate the formula during the proof "on demand" just as far as needed to keep refutation completeness. The clause produced by a resolution rule is sometimes called a resolvent. (en) 논리학에서 분해 증명(Resolution) 혹은 분해법이란 증명의 방법론 중의 하나이다. 1965년에 미국의 (John Alan Robinson)이 공식적으로 제안하였다. 이것은 어떤 두 명제가 논리합으로 이어져 있을 때 다른 명제를 도입하여 증명하는 방법이다. 형식적으로 볼 때, 이는 혹은 삼단논법의 일반화로 볼 수 있다. (ko) 導出原理（どうしゅつげんり、英: resolution principle）とは、により1965年に提案された原理または手法を言う。 導出原理を元とする導出の手法は、その後の定理自動証明に大きな影響を与え、またPrologなどの論理プログラミング言語の基礎となった。 (ja) In de wiskundige logica en bij is resolutie een afleidingsregel die gebruikt wordt voor bewijzen uit het ongerijmde van in de propositie- en predicatenlogica. Resolutie is een geldige regel voor het afleiden van een nieuwe clausule (Engels: clause, een disjunctie van literalen) uit twee clausules die complementaire literalen bevatten. De resolutieregel produceert een nieuwe clausule met alle literalen in beide clausules behalve de complementaire literalen. De geproduceerde clausule wordt een resolvent genoemd. Resolutie wordt in automatische stellingbewijzers gebruikt om de onvervulbaarheid, het ontbreken van een toekenning van waar of onwaar aan de atomaire formules zodat de formule waar is, van een logische formule te bewijzen. Meer informeel gezegd probeert men aan te tonen dat de formule niet waar kan zijn. (nl) O princípio da resolução é uma regra de inferência que dá origem a uma técnica de demonstração por refutação para sentenças e inferências da lógica proposicional e da lógica de primeira ordem. (pt) Пра́вило резолю́ций — это правило вывода, восходящее к методу доказательства теорем через поиск противоречий; используется в логике высказываний и логике первого порядка. Правило резолюций, применяемое последовательно для списка резольвент, позволяет ответить на вопрос, существует ли в исходном множестве логических выражений противоречие. Правило резолюций предложено в 1930 году в докторской диссертации Жака Эрбрана для доказательства теорем в формальных системах первого порядка. Правило разработано Джоном Аланом Робинсоном в 1965 году. Алгоритмы доказательства выводимости , построенные на основе этого метода, применяются во многих системах искусственного интеллекта, а также являются фундаментом, на котором построен язык логического программирования «Пролог». (ru) Rezolucja – metoda automatycznego dowodzenia twierdzeń oparta na generowaniu nowych klauzul, aż dojdzie się do sprzeczności. W ten sposób można udowodnić, że dane twierdzenie nie jest spełnialne, lub też, co jest równoważne, że jego zaprzeczenie jest tautologią. Rezolucja jest podstawą wielu praktycznych systemów dowodzenia twierdzeń rachunku predykatów pierwszego rzędu. (pl) Правило резолюцій — це правило висновування, що сходить до методу доказу теорем через пошук протиріч; використовується в логіці висловлювань і логіці предикатів першого порядку. Правило резолюцій, що застосовується послідовно для списку резольвент, дозволяє відповісти на питання, чи існує у вхідній множині логічих виразів протиріччя. Правило резолюцій запропоновано в 1930 році в докторській дисертації Жака Ербрана для доведення теорем у формальних системах першого порядку. Правило розроблено Джоном Аланом Робінсоном в 1965 році. Алгоритми доказу виводимості , побудовані на основі цього методу, застосовуються в багатьох системах штучного інтелекту, а також є фундаментом, на якому побудовано мову логічного програмування «Пролог». (uk) 归结（resolution）原理，在数理逻辑和自动定理证明中（GOFAI涉及的主题），是对于命题逻辑和一阶逻辑中的句子的推理规则，它导致了一种反证法的定理证明技术。 (zh) |
| dbo:wikiPageExternalLink | https://archive.org/details/symboliclogicmec00chan http://www.cis.upenn.edu/~jean/gbooks/logic.html https://logictools.org |
| dbo:wikiPageID | 2724082 (xsd:integer) |
| dbo:wikiPageLength | 28464 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1124188448 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Universal_quantification dbr:Prover9 dbc:Automated_theorem_proving dbr:Cut_rule dbr:DPLL_algorithm dbr:Unification_(computer_science) dbr:Validity_(logic) dbr:Vampire_(theorem_prover) dbr:Davis–Putnam_algorithm dbr:Inductive_logic_programming dbr:Inverse_resolution dbr:Quantification_(logic) dbr:Consensus_theorem dbc:Proof_theory dbr:Mathematical_logic dbr:Clausal_normal_form dbr:Otter_(theorem_prover) dbr:SPASS dbr:Condensed_detachment dbr:Conjunctive_normal_form dbr:Refutation_completeness dbr:Skolem_function dbc:Propositional_calculus dbr:Clause_(logic) dbr:Completeness_(logic) dbr:Davis-Putnam_algorithm dbr:Propositional_logic dbr:Automated_theorem_proving dbr:Tree_(data_structure) dbr:Data_structure dbr:Gödel's_completeness_theorem dbr:Logic_programming dbr:First-order_logic dbr:Journal_of_the_ACM dbr:Logical_consequence dbr:Proof_by_contradiction dbr:RE_(complexity) dbr:Harper_&_Row dbr:Hilary_Putnam dbr:Atomic_formula dbc:1965_introductions dbr:Tautology_(logic) dbc:Rules_of_inference dbc:Theorems_in_propositional_logic dbr:John_Alan_Robinson dbr:Syllogism dbr:Term_logic dbr:Modus_ponens dbr:Martin_Davis_(mathematician) dbr:Boolean_satisfiability_problem dbr:CARINE dbr:Springer_Science+Business_Media dbr:Ground_instance dbr:Method_of_analytic_tableaux dbr:Search_algorithm dbr:Most_general_unifier dbr:Rule_of_inference dbr:SLD_resolution dbr:SNARK_(theorem_prover) dbr:Soundness dbr:Directed_Acyclic_Graph dbr:Literal_(mathematical_logic) dbr:Existential_quantification dbr:Resolution_inference dbr:List_(data_structure) dbr:Decision_procedure dbr:Unification_(computing) dbr:Predicate_symbol dbr:Theorem-proving dbr:GKC_Theorem_Prover |
| dbp:author | Alex Sakharov (en) |
| dbp:title | Resolution (en) Resolution Principle (en) |
| dbp:urlname | Resolution (en) ResolutionPrinciple (en) |
| dbp:wikiPageUsesTemplate | dbt:Citation_needed dbt:Cite_book dbt:Cite_journal dbt:MathWorld dbt:Reflist dbt:Rp dbt:Short_description dbt:GBurl dbt:Mapsto |
| dct:subject | dbc:Automated_theorem_proving dbc:Proof_theory dbc:Propositional_calculus dbc:1965_introductions dbc:Rules_of_inference dbc:Theorems_in_propositional_logic |
| gold:hypernym | dbr:Rule |
| rdf:type | yago:WikicatTheoremsInPropositionalLogic yago:WikicatRulesOfInference yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Communication100033020 yago:Concept105835747 yago:Content105809192 yago:Idea105833840 yago:Know-how105616786 yago:Message106598915 yago:Method105660268 yago:Proposition106750804 yago:PsychologicalFeature100023100 dbo:Country yago:Rule105846054 yago:Statement106722453 yago:Theorem106752293 yago:WikicatFormalMethods |
| rdfs:comment | Die Resolution ist ein Verfahren der formalen Logik, um eine logische Formel auf Gültigkeit zu testen. Das Resolutionsverfahren, auch Resolutionskalkül genannt, ist ein Widerlegungsverfahren: Statt direkt die Allgemeingültigkeit einer Formel zu zeigen, leitet es einen logischen Widerspruch aus deren Verneinung ab. Diese Herleitung geschieht mittels eines Algorithmus auf rein formalem Weg und kann deshalb von einem Computerprogramm durchgeführt werden. Die Resolution ist eine der bekanntesten Techniken des Maschinengestützten Beweisens. (de) En logique mathématique, la règle de résolution ou principe de résolution de Robinson est une règle d'inférence logique qui généralise le modus ponens. Cette règle est principalement utilisée dans les systèmes de preuve automatiques, elle est à la base du langage de programmation logique Prolog. (fr) En Lógica Resolución es una regla de inferencia utilizada sobre cierto tipo de proposiciones lógicas y es especialmente utilizada para los demostradores automatizados de teoremas. Utilizando resolución se puede construir un demostrador que sea completo (por contradicción) y correcto (en inglés refutational complete and sound) para la lógica proposicional y de primer orden supuesto que un conjunto de proposiciones son insatisfacibles. Por otro lado si el conjunto de proposiciones de hecho es satisfacible, puede o no terminar en una cantidad finita de pasos una demostración por resolución, generalmente lo que sucede es que se asigna un tiempo límite para hallar si un conjunto es insatisfacible o no. (es) 논리학에서 분해 증명(Resolution) 혹은 분해법이란 증명의 방법론 중의 하나이다. 1965년에 미국의 (John Alan Robinson)이 공식적으로 제안하였다. 이것은 어떤 두 명제가 논리합으로 이어져 있을 때 다른 명제를 도입하여 증명하는 방법이다. 형식적으로 볼 때, 이는 혹은 삼단논법의 일반화로 볼 수 있다. (ko) 導出原理（どうしゅつげんり、英: resolution principle）とは、により1965年に提案された原理または手法を言う。 導出原理を元とする導出の手法は、その後の定理自動証明に大きな影響を与え、またPrologなどの論理プログラミング言語の基礎となった。 (ja) O princípio da resolução é uma regra de inferência que dá origem a uma técnica de demonstração por refutação para sentenças e inferências da lógica proposicional e da lógica de primeira ordem. (pt) Rezolucja – metoda automatycznego dowodzenia twierdzeń oparta na generowaniu nowych klauzul, aż dojdzie się do sprzeczności. W ten sposób można udowodnić, że dane twierdzenie nie jest spełnialne, lub też, co jest równoważne, że jego zaprzeczenie jest tautologią. Rezolucja jest podstawą wielu praktycznych systemów dowodzenia twierdzeń rachunku predykatów pierwszego rzędu. (pl) 归结（resolution）原理，在数理逻辑和自动定理证明中（GOFAI涉及的主题），是对于命题逻辑和一阶逻辑中的句子的推理规则，它导致了一种反证法的定理证明技术。 (zh) Rezoluce je v logice metoda automatického dokazování tvrzení zavedená Alanem Robinsonem v roce 1965. Pro výrokovou logiku má tvar , kde a jsou disjunkce literálů. se nazývá resolventou. V predikátové logice má rezoluce podobu , kde je substituce unifikující a . V obecnosti je možné a obecně nutné vybrat a unifikovat víc pozitivních literálů v jedné a víc negovaných literálů ve druhé klauzuli. V logice s rovností se k rezoluci přidává odvozovací pravidlo paramodulace. Na principu rezoluce jsou založeny logické programovací jazyky, například Prolog, který používá a Hornovy klauzule. (cs) In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the (complement of the) Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem. (en) In de wiskundige logica en bij is resolutie een afleidingsregel die gebruikt wordt voor bewijzen uit het ongerijmde van in de propositie- en predicatenlogica. Resolutie is een geldige regel voor het afleiden van een nieuwe clausule (Engels: clause, een disjunctie van literalen) uit twee clausules die complementaire literalen bevatten. De resolutieregel produceert een nieuwe clausule met alle literalen in beide clausules behalve de complementaire literalen. De geproduceerde clausule wordt een resolvent genoemd. (nl) Правило резолюцій — це правило висновування, що сходить до методу доказу теорем через пошук протиріч; використовується в логіці висловлювань і логіці предикатів першого порядку. Правило резолюцій, що застосовується послідовно для списку резольвент, дозволяє відповісти на питання, чи існує у вхідній множині логічих виразів протиріччя. Правило резолюцій запропоновано в 1930 році в докторській дисертації Жака Ербрана для доведення теорем у формальних системах першого порядку. Правило розроблено Джоном Аланом Робінсоном в 1965 році. (uk) Пра́вило резолю́ций — это правило вывода, восходящее к методу доказательства теорем через поиск противоречий; используется в логике высказываний и логике первого порядка. Правило резолюций, применяемое последовательно для списка резольвент, позволяет ответить на вопрос, существует ли в исходном множестве логических выражений противоречие. Правило резолюций предложено в 1930 году в докторской диссертации Жака Эрбрана для доказательства теорем в формальных системах первого порядка. Правило разработано Джоном Аланом Робинсоном в 1965 году. (ru) |
| rdfs:label | Rezoluce (logika) (cs) Resolution (Logik) (de) Resolución (lógica) (es) Règle de résolution (fr) 導出原理 (ja) 분해 증명 (ko) Resolutie (logica) (nl) Resolution (logic) (en) Princípio da resolução (pt) Rezolucja (matematyka) (pl) Правило резолюций (ru) Правило резолюцій (uk) 归结原理 (zh) |
| owl:sameAs | freebase:Resolution (logic) yago-res:Resolution (logic) wikidata:Resolution (logic) dbpedia-cs:Resolution (logic) dbpedia-de:Resolution (logic) dbpedia-es:Resolution (logic) dbpedia-fa:Resolution (logic) dbpedia-fr:Resolution (logic) dbpedia-hu:Resolution (logic) dbpedia-ja:Resolution (logic) dbpedia-ko:Resolution (logic) dbpedia-nl:Resolution (logic) dbpedia-pl:Resolution (logic) dbpedia-pt:Resolution (logic) dbpedia-ru:Resolution (logic) dbpedia-uk:Resolution (logic) dbpedia-zh:Resolution (logic) https://global.dbpedia.org/id/8Eyw |
| prov:wasDerivedFrom | wikipedia-en:Resolution_(logic)?oldid=1124188448&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Resolution_(logic) |
| is dbo:wikiPageDisambiguates of | dbr:Resolution |
| is dbo:wikiPageRedirects of | dbr:First-order_resolution dbr:Resolvent_(logic) dbr:Method_of_resolution dbr:Non-clausal_resolution dbr:Paramodulation dbr:Resolution_inference dbr:Resolution_prover dbr:Robinson`s_resolution_principle dbr:Robinson's_Resolution_Algorithm dbr:First_order_resolution dbr:Binary_resolution dbr:Resolution_principle dbr:Logical_resolution |
| is dbo:wikiPageWikiLink of | dbr:Problem_solving dbr:Program_synthesis dbr:Prolog dbr:Proof_complexity dbr:Factoring dbr:Proof_compression dbr:Answer_set_programming dbr:Archie_Blake_(mathematician) dbr:History_of_artificial_intelligence dbr:List_of_important_publications_in_theoretical_computer_science dbr:Resolution_proof_reduction_via_local_context_rewriting dbr:DPLL_algorithm dbr:Unification_(computer_science) dbr:Davis–Putnam_algorithm dbr:Cancel dbr:Index_of_philosophy_articles_(R–Z) dbr:Inverse_resolution dbr:List_of_programming_languages_by_type dbr:List_of_rules_of_inference dbr:Propositional_proof_system dbr:Consensus_theorem dbr:Narrowing_of_algebraic_value_sets dbr:Otter_(theorem_prover) dbr:Skolem_normal_form dbr:Structural_rule dbr:Glossary_of_artificial_intelligence dbr:Condensed_detachment dbr:Congruence_lattice_problem dbr:Conjunctive_normal_form dbr:Commercial_Court_(Victoria) dbr:Completeness_(logic) dbr:Horn_clause dbr:Mutilated_chessboard_problem dbr:Occurs_check dbr:Automated_theorem_proving dbr:Václav_Chvátal dbr:Logic_of_argumentation dbr:Toniann_Pitassi dbr:Prolog_syntax_and_semantics dbr:Alexander_Razborov dbr:First-order_logic dbr:First-order_resolution dbr:Resolution dbr:Resolvent_(logic) dbr:2-satisfiability dbr:Herbrand_structure dbr:International_Alert dbr:Isabelle_(proof_assistant) dbr:Theory_(mathematical_logic) dbr:Model_elimination dbr:Boolean_satisfiability_algorithm_heuristics dbr:Planner_(programming_language) dbr:Frege_system dbr:Method_of_resolution dbr:Knuth–Bendix_completion_algorithm dbr:Method_of_analytic_tableaux dbr:Wolfgang_Haken dbr:XSB dbr:Proof_calculus dbr:Sequent_calculus dbr:SAT_solver dbr:SLD_resolution dbr:SNARK_(theorem_prover) dbr:Non-clausal_resolution dbr:Literal_(mathematical_logic) dbr:RecycleUnits dbr:Fish_Cheeks dbr:Unit_propagation dbr:Paramodulation dbr:Resolution_proof_compression_by_splitting dbr:Outline_of_logic dbr:Resolution_inference dbr:Resolution_prover dbr:Robinson`s_resolution_principle dbr:Robinson's_Resolution_Algorithm dbr:First_order_resolution dbr:Binary_resolution dbr:Resolution_principle dbr:Logical_resolution |
| is foaf:primaryTopic of | wikipedia-en:Resolution_(logic) |