Publications

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

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

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

Related projects
Title Department Managers
Sintesi di procedure di decisione basate sulla deduzione con applicazioni all'analisi formale automatica di programmi (PRIN 2003) Department Informatica Maria Paola Bonacina
<<back

Activities

Research facilities

Share