Automatyczne dowodzenie twierdzeń




Automatyczne dowodzenie twierdzeń (ang. automated theorem proving) – proces, w którym komputer rozstrzyga czy dane twierdzenie jest dowodliwe w jakiejś teorii, często przy okazji generując jego dowód. Twierdzenia te należą zwykle do rachunku zdań lub rachunku predykatów pierwszego rzędu.


Dla komputera wygodniejsze jest zwykle wnioskowanie w tył, choć czasem stosuje się też wnioskowanie w przód.


Przykładem twierdzenia, które zostało dowiedzione dopiero przez ATP jest "Algebry Robbinsa są boolowskie"[1].




Spis treści






  • 1 Automatyczne dowodzenie twierdzeń rachunku zdań


  • 2 Automatyczne dowodzenie twierdzeń rachunku predykatów


  • 3 Zobacz też


  • 4 Przypisy


  • 5 Linki zewnętrzne





Automatyczne dowodzenie twierdzeń rachunku zdań |


Chodzi o stwierdzenie czy dane twierdzenie jest tautologią, lub czy jest spełnialne. Oba przypadki są wzajemnie połączone: zaprzeczenie twierdzenia jest spełnialne wtedy i tylko wtedy, gdy twierdzenie to nie jest tautologią.


Twierdzenia rachunku zdań zawsze są rozstrzygalne – choćby metodą brute force, która polega na sprawdzeniu 2n kombinacji wartości prawda-fałsz dla n zmiennych zdaniowych występujących w twierdzeniu.


Istnieje wiele innych metod, które mają większą wydajność i generują bardziej czytelne dowody. Do najprostszych z nich należą sekwenty Gentzena, systemy Hilberta oraz dedukcja naturalna. W praktyce używa się zwykle metod bazowanych na procedurze Davisa-Putnama. Można też używać uproszczonych wersji metod dla rachunku predykatów pierwszego rzędu.


Problem spełnialności jest jednak w każdym systemie NP zupełny, zaś problem tautologii – CoNP zupełny.



Automatyczne dowodzenie twierdzeń rachunku predykatów |


Dominujące metody to tableau, a przede wszystkim różne wersje rezolucji. W systemach z równością używa się też paramodulacji. Warto zaznaczyć, że "ogólny" język I rzędu jest nierozstrzygalny. W szczególności nie istnieje algorytm, który dla ogólnego języka I rzędu może określić, czy dane zdanie jest w nim prawdziwe, czy nie. Istnieją jednak "szczególne" języki I rzędu, które są rozstrzygalne. Przykładem rozstrzygalnego języka I rzędu może być arytmetyka liczb rzeczywistych, co udowodnił Alfred Tarski. Do weryfikacji zdań o liczbach rzeczywistych służy metoda eliminacji kwantyfikatorów.



Zobacz też |



  • rachunek lambda

  • CADE

  • CASC

  • subsumpcja

  • unifikacja

  • term

  • indeksowanie termów

  • system wspomagający dowodzenie twierdzeń

  • system Mizar



Przypisy |




  1. ↑ Bernd IB.I. Dahn Bernd IB.I., Robbins Algebras Are Boolean: A Revision of McCune's Computer-Generated Solution of Robbins Problem, „Journal of Algebra”, 208 (2), 1998, s. 526–532, DOI: 10.1006/jabr.1998.7467, ISSN 0021-8693 [dostęp 2018-09-23] .



Linki zewnętrzne |


  • FredericF. Portoraro FredericF., Automated Reasoning [w:] Stanford Encyclopedia of Philosophy [online], CSLI, Stanford University, 20 listopada 2014, ISSN 1095-5054 [dostęp 2018-08-07]  (ang.).



-

這個網誌中的熱門文章

12.7 cm/40 Type 89 naval gun

圖片
12.7 cm/40 Type 89 naval gun Type 89 gun mounted on Chitose Type Naval gun anti-aircraft gun Place of origin Japan Service history In service 1932–45 Used by Imperial Japanese Navy Wars World War II Production history Designed 1928–32 Produced 1932–45 No.  built ~1500 Variants Type 88 Specifications Mass 3,100 kilograms (6,834 lb) Barrel length 5,080 millimeters (16 ft 8 in) (bore length) Shell Fixed Shell weight 20.9–23.45 kilograms (46.1–51.7 lb) Caliber 12.7-centimeter (5.0 in) Breech horizontal breech block Elevation -8° to +90° [1] Rate of fire 8-14 rounds per minute Muzzle velocity 720–725 meters per second (2,360–2,380 ft/s) Maximum firing range 9,440 meters (30,970 ft) at 90° (AA ceiling) 14,800 meters (48,600 ft) at 45° The 12.7 cm/40 Type 89 naval gun was a Japanese anti-aircraft (AA) gun introduced before World War II. It was the Imperial Japanese Navy's standard heavy AA
閱讀完整內容

Shark

圖片
For other uses, see Shark (disambiguation). Sharks Temporal range: Ludfordian-Present, 425–0 Ma PreЄ Є O S D C P T J K Pg N [1] Clockwise from top left: spiny dogfish, Japanese sawshark, whale shark, great white shark, horn shark, frilled shark, scalloped hammerhead and Australian angelshark representing the orders Squaliformes, Pristiophoriformes, Orectolobiformes, Lamniformes, Heterodontiformes, Hexanchiformes, Carcharhiniformes and Squatiniformes respectively. Scientific classification Kingdom: Animalia Phylum: Chordata Class: Chondrichthyes Subclass: Elasmobranchii Infraclass: Euselachii Superorder: Selachimorpha Orders Carcharhiniformes Heterodontiformes Hexanchiformes Lamniformes Orectolobiformes Pristiophoriformes Squaliformes Squatiniformes † Cladoselachiformes † Hybodontiformes † Symmoriida † Xenacanthida (Xenacantiformes) † Elegestolepis † = extinct Synonyms Pleurotremata Sharks
閱讀完整內容

Wiciokrzew

圖片
Wiciokrzew, suchodrzew Morfologia (wiciokrzew pospolity) Systematyka [1] Domena eukarionty Królestwo rośliny Klad rośliny naczyniowe Klad rośliny nasienne Klasa okrytonasienne Klad astrowe Rząd szczeciowce Rodzina przewiertniowate Rodzaj wiciokrzew Nazwa systematyczna Lonicera L. Sp. Pl. 173. 1 Mai 1753 Typ nomenklatoryczny Lonicera caprifolium L. [2] Multimedia w Wikimedia Commons Hasło w Wikisłowniku Kwiaty suchodrzewu pospolitego Owoce suchodrzewu pospolitego Kwiaty wiciokrzewu pomorskiego Kwiaty wiciokrzewu przewiercienia Wiciokrzew , suchodrzew ( Lonicera L.) – rodzaj roślin wieloletnich należący do rodziny przewiertniowatych ( Caprifoliaceae ). Rośliny zielne i pnące nazywane są wiciokrzewami, natomiast krzewy i niewielkie drzewa – suchodrzewami. Rodzaj liczy około 180 gatunków szeroko rozprzestrzenionych na całej półkuli północnej [3] [4]
閱讀完整內容