Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
STP: a simple theorem prover for IBM-PC compatible computers
Ist Teil von
Proceedings of the 1990 ACM SIGSMALL/PC symposium on small systems, 1990, p.98-105
Ort / Verlag
ACM
Erscheinungsjahr
1990
Link zum Volltext
Quelle
ACM Digital Library Complete
Beschreibungen/Notizen
STP (Simple Theorem Prover) was conceived as a tool to help gain a better understanding of the concepts and difficulties involved in producing a generalized automated theorem prover for first-order logic, such as ITP (Interactive Theorem Prover). The project was undertaken on an IBM-PC using Turbo Pascal, version 3, mainly for reasons of hardware availability and software familiarity. ITP is the model on which STP is based. Although STP is functionally much less complex than ITP, they share the same syntax for input clauses. An additional program, called the "Skolemizer", was developed as a user aid to transform generalized first-order logic formulae into their Skolem conjunctive normal form equivalents for input to STP or to ITP. The initial strategy used to search the solution space proved to be inadequate for the development environment, and was later expanded to include a second search strategy option. The current version of STP uses LUSH resolution plus clause factoring to do refutation proofs. It is able to solve most simple problems, but takes too long to solve significant problems. Although STP met its design goal-that of being an educational experience to develop-it needs to be extended to utilize more complex forms of resolution and other related methods. With recent advances in small computer hardware and software capabilities, these enhancements should now be possible.
Sprache
Englisch
Identifikatoren
ISBN: 9780897913478, 0897913477
DOI: 10.1145/99412.99439
Titel-ID: cdi_proquest_miscellaneous_31593373
Format
–
Weiterführende Literatur
Empfehlungen zum selben Thema automatisch vorgeschlagen von bX