Proofs as Schemas and Their Heuristic Use
Automated theorem proving essentially amounts to solving search problems. Despite significant progress in recent years theorem provers still have many shortcomings. The use of machine-learning techniques such as schemas is acknowledged as promising, but difficult to apply in the area of theorem proving. We propose a simple form of schemas, and to make use of a schema heuristically by integrating it with a search-guiding heuristic. Experiments have demonstrated that the approach allows a theorem...[Show more]
|Collections||ANU Research Publications|
|Source:||Journal of Symbolic Computation|
|01_Fuchs_Proofs_as_Schemas_and_Their_2000.pdf||354.48 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.