Brown, Marianne, and Sutcliffe, Geoff (2000) System description: PTTP+GLiDeS semantically guided PTTP. Lecture Notes in Computer Science, 1831. pp. 411-416.

PDF (Published Version) - Published Version Restricted to Repository staff only

Abstract

PTTP+GLiDeS is a semantically guided linear deduction theorem prover, built from PTTP [9] and MACE [7]. It takes problems in clause normal form (CNF), generates semantic information about the clauses, and then uses the semantic information to guide its search for a proof. In the last decade there has been some work done in the area of semantic guidance, in a variety of first order theorem proving paradigms: SCOTT [8] is based on OTTER and is a forward chaining resolution system; CLIN-S [3] uses hyperlinking; RAMCS [2] uses constrained clauses to allow it to search for proofs and models simultaneously; and SGLD [11] is a chain format linear deduction system based on Graph Construction. Of these, CLIN-S and SGLD need to be supplied with semantics by the user. SCOTT uses FINDER [8] to generate models, and RAMCS generates its own models.

Item ID:	486
Item Type:	Article (Research - C1)
ISSN:	1611-3349
Keywords:	automated theorem proving; linear deduction; semantic guidence
Additional Information:	This paper was also presented at the International Conference on Automated Deduction, CADE 17 conducted in Pittsburgh, Pennsylvania 17-20 July 2000.
Date Deposited:	16 Feb 2017 03:41
FoR Codes:	08 INFORMATION AND COMPUTING SCIENCES > 0801 Artificial Intelligence and Image Processing > 080199 Artificial Intelligence and Image Processing not elsewhere classified @ 100%
SEO Codes:	89 INFORMATION AND COMMUNICATION SERVICES > 8902 Computer Software and Services > 890202 Application Tools and System Utilities @ 100%
Downloads:	Total: 4
	More Statistics