LiU Electronic Press
Full-text not available in DiVA
Author:
Szalas, Andrzej (Linköping University, The Institute of Technology) (Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab)
Tyszkiewicz, Jerzy
Title:
On the fixpoint theory of equality and its applications
Department:
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab
Linköping University, The Institute of Technology
Publication type:
Conference paper (Refereed)
Language:
English
In:
Proceedings of the 9th International Conference on Relational Methods in Computer Science and 4th International Workshop on Applications of Kleene Algebra (RelMiCS/AKA)
Publisher: Springer
Series:
Lecture Notes in Computer Science, ISSN 0302-9743; 4136
Volume:
4136
Pages:
388-401
Year of publ.:
2006
URI:
urn:nbn:se:liu:diva-48069
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-48069
Subject category:
Engineering and Technology
SVEP category:
TECHNOLOGY
Keywords(en) :
fixpoint calculus, equality theory, automated reasoning
Abstract(en) :

In the current paper we first show that the fixpoint theory of equality is decidable. The motivation behind considering this theory is that second-order quantifier elimination techniques based on a theorem given in [16], when successful, often result in such formulas. This opens many applications, including automated theorem. proving, static verification of integrity constraints in databases as well as reasoning with weakest sufficient and strongest necessary conditions.

Available from:
2009-10-11
Created:
2009-10-11
Last updated:
2011-02-26
Statistics:
12 hits