SNARK (dowód twierdzeń)
SNARK (SRI's New Automated Reasoning Kit) to dowód twierdzeń dla wielosortowanej logiki pierwszego rzędu przeznaczony do zastosowań w sztucznej inteligencji i inżynierii oprogramowania , opracowany w SRI International .
Główne mechanizmy wnioskowania SNARK to rozdzielczość i paramodulacja ; ponadto oferuje wyspecjalizowane procedury decyzyjne dla poszczególnych dziedzin, np. narzędzie do rozwiązywania ograniczeń dla logiki interwałów czasowych Allena. W przeciwieństwie do wielu innych dowodzenia twierdzeń jest w pełni zautomatyzowany (nieinteraktywny). SNARK oferuje wiele strategicznych elementów sterujących do dostosowywania zachowania wyszukiwania, a tym samym dostrajania jego wydajności do określonych aplikacji. To, wraz z wykorzystaniem wielosortowanej logiki i możliwości integracji procedur wnioskowania specjalnego przeznaczenia z wnioskowaniem ogólnego przeznaczenia, czyni go szczególnie odpowiednim jako rozumowanie dla dużych zestawów twierdzeń.
SNARK jest używany jako element rozumowania w projekcie NASA Intelligent Systems Project . Jest napisany w języku Common Lisp i dostępny na licencji Mozilla Public License .
Zobacz też
- Zautomatyzowane rozumowanie
- Zautomatyzowane dowodzenie twierdzeń
- Dowód wspomagany komputerowo
- Logika pierwszego rzędu
- Weryfikacja formalna
- M. Stickel, R. Waldinger , M. Lowry, T. Pressburger i I. Underwood. „Dedukcyjny skład oprogramowania astronomicznego z bibliotek podprogramów”. Proceedings of the XII International Conference on Automated Deduction (CADE-12) , Nancy, Francja, czerwiec 1994, strony 341–355.
- Richarda Waldingera , Martina Reddy'ego i Jennifer Dungan. „ Dedukcyjny skład wielu źródeł danych ”. Maj 2002 Raport z postępów zadania badawczego Intelligent Data Understanding, Intelligent System Project, NASA SISM.
- R, Waldinger , DE Appelt, J. Fry, DJ Israel, P. Jarvis, D. Martin, S. Riehemann, ME Stickel, M. Tyson, J. Hobbs i JL Dungan. „ Dedukcyjne odpowiadanie na pytania z wielu zasobów. ” w New Directions in Question Answering , AAAI , 2004.
- R. Waldinger , P. Jarvis i J. Dungan. „Korzystanie z dedukcji do choreografii wielu źródeł danych”. W Semantic Web Technologies for Search and Retrieving , Sanibel Island, Floryda, październik 2003.
Linki zewnętrzne