Brown, Marianne Elizabeth (2003) Guiding linear deductions with semantics. Masters (Research) thesis, James Cook University.

Preview	PDF Download (55kB)
Preview	PDF Download (324kB)

Abstract

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.

Item ID:	1184
Item Type:	Thesis (Masters (Research))
Keywords:	Guidance, Automatic Theorem Proving systems, Use of semantic information, Linear deduction systems, Incorporating semantic guidance into model elimination based linear systems, GLiDeS pruning strategy, Good guidance
Date Deposited:	08 Nov 2006
FoR Codes:	08 INFORMATION AND COMPUTING SCIENCES > 0802 Computation Theory and Mathematics > 080201 Analysis of Algorithms and Complexity @ 40% 08 INFORMATION AND COMPUTING SCIENCES > 0801 Artificial Intelligence and Image Processing > 080108 Neural, Evolutionary and Fuzzy Computation @ 40% 08 INFORMATION AND COMPUTING SCIENCES > 0802 Computation Theory and Mathematics > 080204 Mathematical Software @ 20%
Downloads:	Total: 445 Last 12 Months: 21
	More Statistics