| ||||
| ||||
![]() Title:SGGS Decision Procedures Conference:IJCAR 2020 Tags:decidable fragment, decision procedure, decision procedures, finite basis, first order logic, ground preserving, hyperresolution, ordered resolution, SGGS, stratified fragment, term rewriting, termination tool and theorem proving Abstract: 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. | ||||
Copyright © 2002 – 2025 EasyChair |