Publications

On handling distinct objects in the superposition calculus  (2005)

Authors:
Stephan Schulz; Maria Paola Bonacina
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
Nations of authors:
GERMANIA; ITALIA
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
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 Fifth International Workshop on the Implementation of Logics (IWIL) was held as a satellite of the Eleventh International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)
Product ID:
21759
Handle IRIS:
11562/21759
Deposited On:
December 3, 2007
Last Modified:
November 2, 2016
Bibliographic citation:
Stephan Schulz; Maria Paola Bonacina, 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