Decision procedures based on dual tableaux for some logics of binary relations

Seminarium organizowane wspólnie przez Zaklad Logiki Matematycznej Wydziału Matematyki, Informatyki i Mechaniki UW oraz Instytut Łączności 

We consider four fragments of the relational logic RL(1) obtained by posing  some constraints on the terms constructed with the composition operator. In particular, the first argument of the composition can only be a relational variable in the first fragment, a positive Boolean term in the second one, a positive Boolean term involving the inverse operator in the third one, and any term not containing the composition operator in the latter fragment. These logics may serve as formalisms for the representation of various theories, in particular of some non-classical logics including modal and description logics. We show how relational dual tableaux can be used to provide decision procedures for each of them. 

This is joint work with Ewa Orlowska and Domenico Cantone.