Publications

On handling distinct objects in the superposition calculus  (2005)

Authors:
Stephan, Schulz; Bonacina, Maria Paola
Title:
On handling distinct objects in the superposition calculus
Year:
2005
Type of item:
Contributo in atti di convegno
Tipologia ANVUR:
Contributo in Atti di convegno
Language:
Inglese
Format:
A Stampa
Congresso:
Fifth International Workshop on the Implementation of Logics (IWIL), Eleventh International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)
Place:
Montevideo, Uruguay
Period:
March 2005
Page numbers:
66-77
Keyword:
Superposition, unique name assumption
Short description of contents:
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)
Web page:
https://mariapaola.github.io/
Product ID:
21759
Handle IRIS:
11562/21759
Deposited On:
December 3, 2007
Last Modified:
September 18, 2023
Bibliographic citation:
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)Proceedings of "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

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