PTTP+GLiDeS: Guiding linear deductions with semantics

Marianne Brown, Geoffrey Sutcliffe

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

Using semantics to guide automated theorem proving systems is an under-utilised technique. In linear deduction, semantic guidance has received only limited attention. This research is developing semantic guidance for linear deduction in the Model Elimination paradigm. Search pruning, at the possible loss of some refutation completeness, and search guidance, are being considered. This paper describes PTTP+GLiDeS, a PTTP style prover augmented with a semantic pruning mechanism, GLiDeS. PTTP+GLiDeS combines a modified version of Stickel’s PTTP prover with the model generator MACE.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages244-254
Number of pages11
Volume1747
ISBN (Print)3540668225, 9783540668220
DOIs
StatePublished - 1999
Externally publishedYes
Event12th Australian Joint Conference on Artificial Intelligence, AI 1999 - Sydney, Australia
Duration: Dec 6 1999Dec 10 1999

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1747
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other12th Australian Joint Conference on Artificial Intelligence, AI 1999
CountryAustralia
CitySydney
Period12/6/9912/10/99

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'PTTP+GLiDeS: Guiding linear deductions with semantics'. Together they form a unique fingerprint.

Cite this