TPTP

TPTP (Thousands of Problems for Theorem Provers) – biblioteka problemów dla systemów automatycznego dowodzenia twierdzeń^[1]. Obejmuje ponad 15 tysięcy problemów abstrakcyjnych^[2].

Biblioteka operuje własnym językiem Typed Higher-order Form (THF), który jest czytelny dla ludzi, łatwo parsowalny dla komputerów i bazuje na Prologu. Są na niej oparte problemy rozwiązaywane podczas konkursu CADE ATP System Competition^[1]^[3].

Przypisy[edytuj | edytuj kod]

↑ ^a ^b GeoffG. Sutcliffe GeoffG. i inni, Progress in the Development of Automated Theorem Proving for Higher-order Logic, DOI: 10.1007/978-3-642-02959-2_8 (ang.).
↑ Inside the TPTP. tptp.org. [dostęp 2024-04-19]. (ang.).
↑ M. SaqibM.S. Nawaz M. SaqibM.S. i inni, A Survey on Theorem Provers in Formal Methods, DOI: 10.48550/arXiv.1912.03028 (ang.).

Linki zewnętrzne[edytuj | edytuj kod]

Strona www oprogramowania

[Springer-1] GeoffG. Sutcliffe GeoffG. i inni, Progress in the Development of Automated Theorem Proving for Higher-order Logic, DOI: 10.1007/978-3-642-02959-2_8 (ang.).

[TPTPmanual-2] Inside the TPTP. tptp.org. [dostęp 2024-04-19]. (ang.).

[survey-3] M. SaqibM.S. Nawaz M. SaqibM.S. i inni, A Survey on Theorem Provers in Formal Methods, DOI: 10.48550/arXiv.1912.03028 (ang.).

[1]

[2]

[3]