System description: PTTP+GLiDeS semantically guided PTTP

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

[img] PDF (Published Version) - Published Version
Restricted to Repository staff only

View at Publisher Website:


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

Actions (Repository Staff Only)

Item Control Page Item Control Page