Pubblicazioni

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

Autori:
Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz
Titolo:
Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures
Anno:
2005
Tipologia prodotto:
Contributo in atti di convegno
Tipologia ANVUR:
Contributo in Atti di convegno
Lingua:
Inglese
Formato:
A Stampa
Titolo del Convegno:
3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Seventeenth International Conference on Computer Aided Verification (CAV)
Luogo:
Edinburgh, Scotland, U.K.
Periodo:
July 2005
Intervallo pagine:
33-41
Parole chiave:
Satisfiability modulo theories, superposition, decision procedures
Breve descrizione dei contenuti:
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").
Note:
The 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR) was held as a satellite of the 17th International Conference on Computer Aided Verification (CAV)
Pagina Web:
https://mariapaola.github.io/
Id prodotto:
23780
Handle IRIS:
11562/23780
depositato il:
6 dicembre 2007
ultima modifica:
18 settembre 2023
Citazione bibliografica:
Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz, Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures  in Proceedings of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR)Atti di "3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Seventeenth International Conference on Computer Aided Verification (CAV)" , Edinburgh, Scotland, U.K. , July 2005 , 2005pp. 33-41

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo IRIS

Progetti Collegati
Titolo Dipartimento Responsabili
Sintesi di procedure di decisione basate sulla deduzione con applicazioni all'analisi formale automatica di programmi (PRIN 2003) Dipartimento Informatica Maria Paola Bonacina
<<indietro

Attività

Strutture

Condividi