Pubblicazioni

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 , 2005 , pp. 33-41

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