| dbpprop:abstract
|
- In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic. In other words, iteratively applying the resolution rule in a suitable way allows for telling whether a propositional formula is satisfiable and for proving that a first-order formula is unsatisfiable; this method may prove the satisfiability of a first-order satisfiable formula, but not always, as it is the case for all methods for first-order logic. Resolution was introduced by John Alan Robinson in 1965.
- 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.
- La règle de résolution ou principe de résolution de Robinson est une règle d'inférence logique que l'on peut voir comme une généralise du 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.
- A rezolúció a matematikai logikában egy levezetési eljárás, mely alapja az egyik automatikus tételbizonyítási módszernek, elméletnek, a rezolúciós kalkulusnak. Az eljárás az informatikában is jelentős, mivel a logikai programozás alapnyelve, a Prolog a rezolúció egy fajtájának, az elsőrendű lineáris rezolúciónak az algoritmikus megvalósítása. A rezolúció szintaktikus módszer (az eljárás kiinduló formuláinak alakja, felépítése alapján működik); alapja, hogy két logikai formulához hozzárendeljük egy speciális következményformulájukat, az ún. rezolvensüket. A rezolválandó formulákat először konjunktív normálforma alakúra kell hozni. Erre létezik automatikus eljárás; bár a logikai programozási nyelvek általában már feltételezik, hogy ez megtörtént, és csak speciális alakú formulákkal (ún. programklózok) tudnak dolgozni.
- 導出（どうしゅつ）とは、数理論理学における一つの演繹方法である。定理自動証明において一般的に使われる手法。 導出おいて二つの節より新しい節を導きだす演繹ルールを導出原理といい、一方の節に含まれる命題と、他方の節に含まれるその命題の否定をのぞき、その他の命題の論理和をとることで、新しい節を得ることをいう。式で表せば、命題<math>a_i</math>が命題<math>b_j</math>の否定である時、 <math>\frac{ a_1 \lor \ldots \vee a_{i-1} \vee a_i \vee a_{i+1} \vee \ldots \lor a_n, \quad b_1 \lor \ldots \vee b_{j-1} \vee b_j \vee b_{j+1} \vee \ldots \lor b_m} {a_1 \lor \ldots \lor a_{i-1} \lor a_{i+1} \lor \ldots \lor a_n \lor b_1 \lor \ldots \lor b_{j-1} \lor b_{j+1} \lor \ldots \lor b_m}</math> と書ける。 導出は与えられた節の集合に、導出原理を当てはめ得られる新しい節をもとの節の集合に加える事を繰り返す事で行われる。命題論理、また述語論理いずれにも使う事が出来る。命題論理における導出は完全である。 プログラミング言語のPrologの基礎となる理論である。
- In wiskundige logica en bij automatisch stelling bewijzen is resolutie is een afleidingsregel die gebruikt wordt bij reductio ad absurdum bewijzen voor zinnen in propositielogica en predicatenlogica. Resolutie is een geldige regel voor het afleiden van een nieuwe clausule uit twee clausules die complementaire literals bevatten. De resolutieregel produceert een nieuwe clausule met alle literals in beide clausules behalve de complementaire literals. 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. Resolutie kan wel gebruikt worden om te onderzoeken of een formule vervulbaar is maar om het te bewijzen zijn andere technieken nodig, zoals semantische tableaus of zogeheten satisfiability checkers die een toekenning van waar of onwaar proberen te vinden zodat de formule waar wordt.
- Rezolucja to 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ą. Zasady generowania nowych klauzul to: Z klauzuli [ α ∧ β, Γ ] można utworzyć [ α, Γ ] i [ β, Γ ] Z klauzuli [ α ∨ β, Γ ] można utworzyć [ α, β, Γ ] Z pary klauzul [ α, Γ ] i [ ¬ β, Δ ], gdzie α i β się unifikują, σ zaś jest ich najmniejszym unifikatorem - [ σ(Γ); σ(Δ) ] (zasada rezolucji) Gdzie α, β to formuły, Γ, Δ - zbiory formuł. W rachunku zdań reguła rezolucji upraszcza się do: Z pary klauzul [ α, Γ ] i [ ¬ α, Δ ] można utworzyć [ Γ, Δ ] Jeśli potrafimy dojść do klauzuli pustej rezolucja jest zakończona, i twierdzenie jest sprzeczne (a więc jego zaprzeczenie jest tautologią). Przykład działania. Udowodnimy że p → (p ∨ q): Sprowadźmy najpierw ¬ (p →) do postaci z negacjami na liściach (nie jest to konieczne, ale potrzebne by były wtedy reguły usuwania każdego ze spójników oraz podwójnej negacji): ¬ (p →) ¬ (∨) p ∧ (¬) p ∧ (∧) Rezolucja w działaniu: [p ∧ (∧)] [p] - z 1 [(¬ p) ∧ (¬ q)] - z 1 [¬ p] - z 3 - z 2,4 i reguły rezolucji Istnieje wiele wersji pochodnych rezolucji, polegających na ograniczeniu możliwości stosowania reguły rezolucji w prowadzaniu dodatkowych reguł (takich jak faktoryzacja czy kondensacja), co daje lepsze praktyczne rezultaty. Rezolucja jest podstawą wielu praktycznych systemów dowodzenia twierdzeń rachunku predykatów pierwszego rzędu.
- 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.
- Пра́вило резолю́ций — правило вывода в исчислении высказываний и исчислении предикатов.
- 在数理逻辑和自动定理证明中，归结(resolution)是对于命题逻辑和一阶逻辑中的句子的推理规则，它导致了一种反证法的定理证明技术。
|
| rdfs:comment
|
- In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic.
- 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.
- La règle de résolution ou principe de résolution de Robinson est une règle d'inférence logique que l'on peut voir comme une généralise du 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.
- A rezolúció a matematikai logikában egy levezetési eljárás, mely alapja az egyik automatikus tételbizonyítási módszernek, elméletnek, a rezolúciós kalkulusnak. Az eljárás az informatikában is jelentős, mivel a logikai programozás alapnyelve, a Prolog a rezolúció egy fajtájának, az elsőrendű lineáris rezolúciónak az algoritmikus megvalósítása.
- In wiskundige logica en bij automatisch stelling bewijzen is resolutie is een afleidingsregel die gebruikt wordt bij reductio ad absurdum bewijzen voor zinnen in propositielogica en predicatenlogica. Resolutie is een geldige regel voor het afleiden van een nieuwe clausule uit twee clausules die complementaire literals bevatten. De resolutieregel produceert een nieuwe clausule met alle literals in beide clausules behalve de complementaire literals.
- Rezolucja to 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ą.
- 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.
- Пра́вило резолю́ций — правило вывода в исчислении высказываний и исчислении предикатов.
- 在数理逻辑和自动定理证明中，归结(resolution)是对于命题逻辑和一阶逻辑中的句子的推理规则，它导致了一种反证法的定理证明技术。
|
![[RDF Data]](/statics/sw-cube.png)
