A Completeness Result for Relation Algebra with Binders

AbstractThis paper presents an axiom system to Relation Algebra with Binders. This is a hybrid formalism introduced to fix the equipollence problems in Tarski's Relational Calculus. RAB does not fill the requirements imposed by Tarski, but as it was showed that is a very interesting alternative to First-Order Logic when concerning the symbolization of statements about binary relations. The presentation of an axiomatization of RAB contributes to its development as a formalism to the inference of facts about relations. Relational calculi have been extensively applied as much in Computer Science as in Natural Language studies and the classical theory has been extended to many directions. Since RAB seems provide new perspectives on the application of both Relation Algebra and Hybrid Logic, the work in this paper could be considered as a contribution to that development