The theory of idempotent semigroups is of unification type zero

1986 ◽  
Vol 2 (3) ◽  
pp. 283-286 ◽  
Author(s):  
Franz Baader
Keyword(s):  
Unification Type

scholarly journals UNIFICATION IN INTERMEDIATE LOGICS

2015 ◽  
Vol 80 (3) ◽  
pp. 713-729 ◽  
Author(s):  
ROSALIE IEMHOFF ◽  
PAUL ROZIÈRE
Keyword(s):  
Intermediate Logics ◽  
Unification Type

AbstractThis paper contains a proof–theoretic account of unification in intermediate logics. It is shown that many existing results can be extended to fragments that at least contain implication and conjunction. For such fragments, the connection between valuations and most general unifiers is clarified, and it is shown how from the closure of a formula under the Visser rules a proof of the formula under a projective unifier can be obtained. This implies that in the logics considered, for the n-unification type to be finitary it suffices that the m-th Visser rule is admissible for a sufficiently large m. At the end of the paper it is shown how these results imply several well-known results from the literature.

Unification in intuitionistic logic

1999 ◽  
Vol 64 (2) ◽  
pp. 859-880 ◽  
Author(s):  
Silvio Ghilardi
Keyword(s):  
Intuitionistic Logic ◽  
Heyting Algebras ◽  
Unification Type ◽  
Finitely Presented

AbstractWe show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.

scholarly journals Preserving Filtering Unification by Adding Compatible Operations to Some Heyting Algebras

2016 ◽  
Vol 45 (3/4) ◽  
Author(s):  
Wojciech Dzik ◽  
Sándor Radeleczki
Keyword(s):  
Residuated Lattices ◽  
Heyting Algebras ◽  
Direct Products ◽  
Unification Type

We show that adding compatible operations to Heyting algebras and to commutative residuated lattices, both satisfying the Stone law ¬x ⋁ ¬¬x = 1, preserves filtering (or directed) unification, that is, the property that for every two unifiers there is a unifier more general then both of them. Contrary to that, often adding new operations to algebras results in changing the unification type. To prove the results we apply the theorems of [9] on direct products of l-algebras and filtering unification. We consider examples of frontal Heyting algebras, in particular Heyting algebras with the successor, γ and G operations as well as expansions of some commutative integral residuated lattices with successor operations.

A note on unification type zero

1988 ◽  
Vol 27 (2) ◽  
pp. 91-93 ◽  
Author(s):  
Franz Baader
Keyword(s):  
Unification Type

scholarly journals About the Unification Type of Modal Logics Between $$\mathbf {KB}$$ and $$\mathbf {KTB}$$

Studia Logica ◽  
2019 ◽  
Vol 108 (5) ◽  
pp. 941-966
Author(s):  
Philippe Balbiani ◽  
Çiğdem Gencer
Keyword(s):  
Modal Logics ◽  
Unification Type
Sign in / Sign up

Export Citation Format

Share Document