Pubblicazioni

On handling distinct objects in the superposition calculus  (2005)

Autori:
Stephan, Schulz; Bonacina, Maria Paola
Titolo:
On handling distinct objects in the superposition calculus
Anno:
2005
Tipologia prodotto:
Contributo in atti di convegno
Tipologia ANVUR:
Contributo in Atti di convegno
Lingua:
Inglese
Formato:
A Stampa
Titolo del Convegno:
Fifth International Workshop on the Implementation of Logics (IWIL), Eleventh International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)
Luogo:
Montevideo, Uruguay
Periodo:
March 2005
Intervallo pagine:
66-77
Parole chiave:
Superposition, unique name assumption
Breve descrizione dei contenuti:
Many domains of reasoning include a set of distinct objects. For general-purpose automated theorem provers, this property has to be specified explicitly, by including distinctness axioms. Since their number grows quadratically with the number of distinct objects, this results in large and clumsy specifications, that may affect performance adversely. We show that object distinctness can be handled directly by a modified superposition-based inference system, including additional inference rules. The new calculus is shown to be sound and complete. A preliminary implementation shows promising results in the theory of arrays.
Note:
The 5th International Workshop on the Implementation of Logics (IWIL) was held as a satellite of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)
Pagina Web:
https://mariapaola.github.io/
Id prodotto:
21759
Handle IRIS:
11562/21759
depositato il:
3 dicembre 2007
ultima modifica:
18 settembre 2023
Citazione bibliografica:
Stephan, Schulz; Bonacina, Maria Paola, On handling distinct objects in the superposition calculus  in Notes of the Fifth International Workshop on the Implementation of Logics (IWIL)Atti di "Fifth International Workshop on the Implementation of Logics (IWIL), Eleventh International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)" , Montevideo, Uruguay , March 2005 , 2005pp. 66-77

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