PTTP+GLiDeS

Guiding linear deductions with semantics

Marianne Brown, Geoffrey Sutcliffe

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

2 Citations (Scopus)

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

Fingerprint

Deduction
Semantics
Guidance
Pruning
Automated Theorem Proving
Theorem proving
Elimination
Completeness
Paradigm
Generator
Model

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Brown, M., & Sutcliffe, G. (1999). PTTP+GLiDeS: Guiding linear deductions with semantics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1747, pp. 244-254). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1747). Springer Verlag. https://doi.org/10.1007/3-540-46695-9_21

PTTP+GLiDeS : Guiding linear deductions with semantics. / Brown, Marianne; Sutcliffe, Geoffrey.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1747 Springer Verlag, 1999. p. 244-254 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1747).

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

Brown, M & Sutcliffe, G 1999, PTTP+GLiDeS: Guiding linear deductions with semantics. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 1747, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1747, Springer Verlag, pp. 244-254, 12th Australian Joint Conference on Artificial Intelligence, AI 1999, Sydney, Australia, 12/6/99. https://doi.org/10.1007/3-540-46695-9_21
Brown M, Sutcliffe G. PTTP+GLiDeS: Guiding linear deductions with semantics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1747. Springer Verlag. 1999. p. 244-254. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-46695-9_21
Brown, Marianne ; Sutcliffe, Geoffrey. / PTTP+GLiDeS : Guiding linear deductions with semantics. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1747 Springer Verlag, 1999. pp. 244-254 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{d2c7d144aafe4d1cad13922482ee5b24,
title = "PTTP+GLiDeS: Guiding linear deductions with semantics",
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.",
author = "Marianne Brown and Geoffrey Sutcliffe",
year = "1999",
doi = "10.1007/3-540-46695-9_21",
language = "English (US)",
isbn = "3540668225",
volume = "1747",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "244--254",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - PTTP+GLiDeS

T2 - Guiding linear deductions with semantics

AU - Brown, Marianne

AU - Sutcliffe, Geoffrey

PY - 1999

Y1 - 1999

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

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

UR - http://www.scopus.com/inward/record.url?scp=84957682309&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84957682309&partnerID=8YFLogxK

U2 - 10.1007/3-540-46695-9_21

DO - 10.1007/3-540-46695-9_21

M3 - Conference contribution

SN - 3540668225

SN - 9783540668220

VL - 1747

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 244

EP - 254

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

ER -