Contact Logic is finitary for unification with constants

Philippe Balbiani (1, 2) , Cigdem Gencer (3)

1 IRIT-LILaC - Logique, Interaction, Langue et Calcul
2 CNRS - Centre National de la Recherche Scientifique
3 Istanbul University

Contact Logic is a formalism for reasoning about the relation of contact between regions. We introduce a new inference problem for Contact Logic, the unification problem, which extends the validity problem by allowing one to replace variables by terms before testing for validity. Our main result is the proof that unification with constants in Contact Logic is finitary.

Mots clés: contact Logic; unification with constants; unification type

Domaines: Logique en informatique [cs.LO]

Philippe Balbiani, Cigdem Gencer. Contact Logic is finitary for unification with constants. International Workshop on Logic and Cognition (WOLC 2016), Dec 2016, Canton, China. ⟨hal-02936482⟩