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

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.
Theorem proving, Model building, SGGS, Horn theories
File in questo prodotto:
File Dimensione Formato  
paper6CEURversion.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Versione dell'editore
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1070206
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact