Sun, 27 Jul 2008 08:05:54 BST CiteULike: gabgas's semantic http://www.citeulike.org/user/gabgas/tag/semantic CiteULike.org en-gb Copyright © 2004-2008 citeulike.org http://www.citeulike.org/user/gabgas/article/2214607 <i></i><br /><br />this paper we report one line of attack on the focus problem for saturation methods of first order theorem proving, by injecting semantic information into heuristics for ordering the possible inferences. Preliminary work on this idea, 1 in collaboration with Lusk, McCune and others, resulted in the system Scott [5, 1, 7] which showed some modest e#ciency gains relative to its parent Otter. However, the main technique used in that prover was model resolution; the work on false preference (see... Semantic Guidance for Saturation-Based Theorem Proving Kahlil Hodgson John Slaney 2008-01-10T14:36:51-00:00 guidance semantic