Séminaire du LIM (LIF et LSIS)
Jeudi 13 septembre à 14h - CMI, Salle de séminaires
John Slaney
Australian National University, Canberra
Development of a Semantically Guided Theorem Prover
This talk reports recent experimental work in the development and refinement of the first order theorem prover SCOTT-5. This is descended from the SCOTT (Semantically Constrained OTTER) prover (see Proc. IJCAI 1993, pp. 109-114) and uses the same combination of a saturation-based theorem prover and a finite domain constraint solver, but the architecture of SCOTT-5 is radically different from that of its ancestor. Here we explain the conceptual basis of semantic guidance as it occurs in SCOTT-5, and give experimental evidence of an improvement in performance (in terms of efficiency) that we attribute to the guidance strategy.
This a joint work with Kahlil Hodgson.
Adresse web de John Slaney : http://arp.anu.edu.au/~jks/