SGGS Decision Procedures

SGGS (Semantically-Guided Goal-Sensitive reasoning) is a conflict-driven first-order theorem-proving method which is refutationally complete and model complete in the limit. These features make it attractive as a basis for decision procedures. In this paper we show that SGGS decides the stratified f...

Descripción completa

Detalles Bibliográficos
Autores principales: Bonacina, Maria Paola, Winkler, Sarah
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324225/
http://dx.doi.org/10.1007/978-3-030-51074-9_20
_version_ 1783551896316805120
author Bonacina, Maria Paola
Winkler, Sarah
author_facet Bonacina, Maria Paola
Winkler, Sarah
author_sort Bonacina, Maria Paola
collection PubMed
description SGGS (Semantically-Guided Goal-Sensitive reasoning) is a conflict-driven first-order theorem-proving method which is refutationally complete and model complete in the limit. These features make it attractive as a basis for decision procedures. In this paper we show that SGGS decides the stratified fragment which generalizes EPR, the PVD fragment, and a new fragment that we dub restrained. The new class has the small model property, as the size of SGGS-generated models can be upper-bounded, and is also decided by hyperresolution and ordered resolution. We report on experiments with a termination tool implementing a restrainedness test, and with an SGGS prototype named Koala.
format Online
Article
Text
id pubmed-7324225
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73242252020-06-30 SGGS Decision Procedures Bonacina, Maria Paola Winkler, Sarah Automated Reasoning Article SGGS (Semantically-Guided Goal-Sensitive reasoning) is a conflict-driven first-order theorem-proving method which is refutationally complete and model complete in the limit. These features make it attractive as a basis for decision procedures. In this paper we show that SGGS decides the stratified fragment which generalizes EPR, the PVD fragment, and a new fragment that we dub restrained. The new class has the small model property, as the size of SGGS-generated models can be upper-bounded, and is also decided by hyperresolution and ordered resolution. We report on experiments with a termination tool implementing a restrainedness test, and with an SGGS prototype named Koala. 2020-05-30 /pmc/articles/PMC7324225/ http://dx.doi.org/10.1007/978-3-030-51074-9_20 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Bonacina, Maria Paola
Winkler, Sarah
SGGS Decision Procedures
title SGGS Decision Procedures
title_full SGGS Decision Procedures
title_fullStr SGGS Decision Procedures
title_full_unstemmed SGGS Decision Procedures
title_short SGGS Decision Procedures
title_sort sggs decision procedures
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324225/
http://dx.doi.org/10.1007/978-3-030-51074-9_20
work_keys_str_mv AT bonacinamariapaola sggsdecisionprocedures
AT winklersarah sggsdecisionprocedures

Ejemplares similares