{"id":{"repo_id":"jamescook","oai_identifier":"oai:researchonline.jcu.edu.au:1184"},"canonical_url":"https://search.dev.ndltd.org/etd/jamescook/oai:researchonline.jcu.edu.au:1184","repository":{"repo_id":"jamescook","name":"James Cook University","base_url":"https://researchonline.jcu.edu.au/cgi/oai2"},"display":{"title":"Guiding linear deductions with semantics","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Brown, Marianne Elizabeth"],"institution":"James Cook University","degree_name":null,"degree_level":"rmasters","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2003,"date_issued":"2003","date_published":"2003","updated_at":"2026-08-21T16:45:46Z","subjects":[],"languages":["en"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":null,"outbound_label":null,"outbound_source":null},"source_record":{"url":"https://researchonline.jcu.edu.au/cgi/oai2?verb=GetRecord&metadataPrefix=uketd_dc&identifier=oai%3Aresearchonline.jcu.edu.au%3A1184","prefix":"uketd_dc"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Brown, Marianne Elizabeth"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2003"]},{"key":"dc:date.issued","label":"Date","values":["2003"]},{"key":"dc:publisher.department","label":"Dc Publisher Department","values":["School of Information Technology"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["James Cook University"]},{"key":"dc:relation.isreferencedby","label":"Dc Relation Isreferencedby","values":["https://researchonline.jcu.edu.au/1184/"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["rmasters"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://researchonline.jcu.edu.au/1184/1/01front.pdf","https://researchonline.jcu.edu.au/1184/2/02whole.pdf"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Guiding linear deductions with semantics"]}]}],"canonical_facts":{"dc:creator":["Brown, Marianne Elizabeth"],"dc:date":["2003"],"dc:date.issued":["2003"],"dc:description.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."],"dc:format":["application/pdf"],"dc:identifier.uri":["https://researchonline.jcu.edu.au/1184/1/01front.pdf","https://researchonline.jcu.edu.au/1184/2/02whole.pdf"],"dc:language":["en"],"dc:publisher.department":["School of Information Technology"],"dc:publisher.institution":["James Cook University"],"dc:relation.isreferencedby":["https://researchonline.jcu.edu.au/1184/"],"dc:title":["Guiding linear deductions with semantics"],"dc:type":["Thesis"],"dc:type.qualificationlevel":["rmasters"]},"updated_at":"2026-08-21T16:45:46Z"}