We prove that the unification type of Lukasiewicz logic with a finite number of variables is either infinitary or nullary. To achieve this result we use Ghilardi’s categorical characterisation of unification types in terms of projective objects, the categorical duality between finitely presented MV-algebras and rational polyhedra, and a homotopy-theoretic argument.
Unification in L ukasiewicz Logic with a Finite Number of Variables
Marco Abbadini;Federica Di Stefano;Luca Spada
2020-01-01
Abstract
We prove that the unification type of Lukasiewicz logic with a finite number of variables is either infinitary or nullary. To achieve this result we use Ghilardi’s categorical characterisation of unification types in terms of projective objects, the categorical duality between finitely presented MV-algebras and rational polyhedra, and a homotopy-theoretic argument.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
