Skip to main content

1999 | OriginalPaper | Buchkapitel

Automatic Generation of Proof Search Strategies for Second-Order Logic

verfasst von : Raul H. C. Lopes

Erschienen in: Automated Deduction — CADE-16

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

P2 is introduced: an algorithm for the automatic generation of proof search strategies from sets of examples of proofs. The proof search strategies are generated as sets of assertions (called methods) about the use of inference rules found in the examples. Sets of methods are prioritized and they can be compiled into clauses of a logic program. Proofs obtained for difficult problems in classical second-order logic are used as evidence of the adequacy of the methodology.

Metadaten
Titel
Automatic Generation of Proof Search Strategies for Second-Order Logic
verfasst von
Raul H. C. Lopes
Copyright-Jahr
1999
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-48660-7_40

Neuer Inhalt