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
閱讀完整內容

University of Vienna

圖片
"Vienna University" redirects here. For Vienna University of Economics and Business, see Vienna University of Economics and Business. University of Vienna Universität Wien Type Public Established 1365 Budget € 544 million [1] Rector Heinz Engl Academic staff 6,765 Administrative staff 3,106 Students 94,000 [2] Postgraduates 16,490 Doctoral students 8,945 Location Main building, Vienna , Austria 48°12′47″N 16°21′35″E  /  48.21306°N 16.35972°E  / 48.21306; 16.35972 Coordinates: 48°12′47″N 16°21′35″E  /  48.21306°N 16.35972°E  / 48.21306; 16.35972 Campus Urban Colors Blue and White           Affiliations Campus Europae, EUA, UNICA Website www.univie.ac.at/en Data as of 2016 [update] The University of Vienna (German: Universität Wien ) is a public university located in Vienna, Austria. It was founded by Duke Rudolph IV in 1365 and is one of the oldest universities in the Ge
閱讀完整內容

Rikitea

圖片
Town in French Polynesia, France Rikitea Town Rikitea Location in French Polynesia Coordinates: 23°7′13″S 134°58′9″W  /  23.12028°S 134.96917°W  / -23.12028; -134.96917 Coordinates: 23°7′13″S 134°58′9″W  /  23.12028°S 134.96917°W  / -23.12028; -134.96917 Country   France Overseas collectivity   French Polynesia Territory Gambier Islands Island Mangareva Rikitea is a small town on Mangareva, which is part of the Gambier Islands in French Polynesia. A majority of the islanders live in Rikitea. [1] [2] The island was a protectorate of France in 1871 and was annexed in 1881. [3] Contents 1 History 2 Geography 3 Economy 4 Landmarks 5 Transportation 6 References 7 Bibliography 8 External links History The town's history dates to the era when the island was first settled with people from the Marquesas Islands in 1100 AD. Captain James Wilson of the London Missionary Society arrived in 1797 on Du
閱讀完整內容