SGGS (Semantically-Guided Goal-Sensitive reasoning) is a refutationally complete theorem-proving method that offers first-order conflict-driven reasoning and is model complete in the limit. This paper investigates the behavior of SGGS on Horn clauses, which are widely used in declarative programming, knowledge representation, and verification. We show that SGGS generates the least Herbrand model of a set of definite clauses, and that SGGS terminates on Horn clauses if and only if hyperresolution does, with the advantage that SGGS builds a model. We report on experiments applying the SGGS prototype prover Koala to Horn problems, with promising performances especially on satisfiable inputs.
On SGGS and Horn clauses
Maria Paola Bonacina
;
2022-01-01
Abstract
SGGS (Semantically-Guided Goal-Sensitive reasoning) is a refutationally complete theorem-proving method that offers first-order conflict-driven reasoning and is model complete in the limit. This paper investigates the behavior of SGGS on Horn clauses, which are widely used in declarative programming, knowledge representation, and verification. We show that SGGS generates the least Herbrand model of a set of definite clauses, and that SGGS terminates on Horn clauses if and only if hyperresolution does, with the advantage that SGGS builds a model. We report on experiments applying the SGGS prototype prover Koala to Horn problems, with promising performances especially on satisfiable inputs.File | Dimensione | Formato | |
---|---|---|---|
PAAR-FLOC2022sggsHorn.pdf
accesso aperto
Descrizione: Articolo
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
925.88 kB
Formato
Adobe PDF
|
925.88 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.