The application of automated reasoning to verification has long shown the importance of decision procedures for satisfiability in decidable theories. The "big engine" approach aims at procedures for the (semi-decidable) validity problem in full first-order logic (with equality), and applies them across all theories that can be presented in the logic. The "little engine" approach aims at procedures for specific decidable theories, by building each theory into a dedicated inference engine. This extended abstract reports on on-going research that aims at replacing the apparent dichotomy ("little engines versus big engines") by a cross-fertilization ("big engines as little engines").

Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures

BONACINA, Maria Paola
;
2005-01-01

Abstract

The application of automated reasoning to verification has long shown the importance of decision procedures for satisfiability in decidable theories. The "big engine" approach aims at procedures for the (semi-decidable) validity problem in full first-order logic (with equality), and applies them across all theories that can be presented in the logic. The "little engine" approach aims at procedures for specific decidable theories, by building each theory into a dedicated inference engine. This extended abstract reports on on-going research that aims at replacing the apparent dichotomy ("little engines versus big engines") by a cross-fertilization ("big engines as little engines").
2005
Satisfiability modulo theories, superposition, decision procedures
File in questo prodotto:
File Dimensione Formato  
PDPAR-CAV2005engines.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 147.94 kB
Formato Adobe PDF
147.94 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/23780
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact