Publications

Authors:

Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz

Title:

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

Year:

2005

Type of item:

Contributo in atti di convegno

Tipologia ANVUR:

Contributo in Atti di convegno

Language:

Inglese

Format:

A Stampa

Congresso:

3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Seventeenth International Conference on Computer Aided Verification (CAV)

Place:

Edinburgh, Scotland, U.K.

Period:

July 2005

Page numbers:

33-41

Keyword:

Satisfiability modulo theories, superposition, decision procedures

Short description of contents:

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)

Web page:

https://mariapaola.github.io/

Product ID:

23780

Handle IRIS:

11562/23780

Deposited On:

December 6, 2007

Last Modified:

September 18, 2023

Bibliographic citation:

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) , Proceedings of "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