Guiding linear deductions with semantics

Guidance is a central issue in Automatic Theorem Proving systems due to the enormity of the search space that these systems navigate. Semantic guidance uses semantic information to direct the path an ATP system takes through the search space. The use of semantic information is potentially more powerful than syntactic information for guidance. This research aimed to discover a method for incorporating semantic guidance into linear deduction systems, in particular model elimination based linear systems. This has been achieved. The GLiDeS pruning strategy is a simple strategy of restricting the model elimination deduction to one where all A-literals are false in the guiding model. This can be easily incorporated into any model elimination based prover. Evaluation of the GLiDeS strategy has shown that when “good guidance” has been achieved, the benefit of this guidance is significant. However attempts to develop a heuristic for predicting which model will provide “good guidance” has been largely unsuccessful.

Level dc:type.qualificationlevel

rmasters

Grantor dc:publisher.institution

James Cook University

Year dc:date.issued

2003

Author dc:creator

• Brown, Marianne Elizabeth

Language dc:language

en