Semantic Guidance for Saturation-Based Theorem Proving

View FullText article

CiteSeer (at Penn State), CiteSeer (at MIT), CiteSeer (at Zurich), CiteSeer (at Singapore)

Reviews [Write a review of this article]

There are no reviews of this article

Notes for this article

gabgas has 1 private note and 0 public notes for this article. If you are gabgas then you can log in to see the private note.

Find related articles from these CiteULike users

gabgas

Find related articles with these CiteULike tags

guidance, semantic

Abstract

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...

@misc{citeulike:2214607, abstract = {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...}, author = {Hodgson, Kahlil and Slaney, John }, citeulike-article-id = {2214607}, keywords = {guidance, semantic}, posted-at = {2008-01-10 14:37:00}, priority = {0}, title = {Semantic Guidance for Saturation-Based Theorem Proving}, url = {http://citeseer.ist.psu.edu/486664.html} }

RIS record

TY - GEN ID - citeulike:2214607 L3 - citeulike-article-id:2214607 TI - Semantic Guidance for Saturation-Based Theorem Proving N2 - 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... KW - guidance KW - semantic AU - Hodgson, Kahlil AU - Slaney, John UR - http://citeseer.ist.psu.edu/486664.html ER -

RIS BibTeX