Checking Admissibility in Finite Algebras Christoph Röthlisberger✯ Mathematics Institute, University of Bern Sidlerstrasse 5, 3012 Bern, Switzerland christoph.roethlisberger@math.unibe.ch Abstract. Checking if a quasiequation is admissible in a finite algebra is a decidable problem, but the naive approach, i.e., checking validity in the corresponding free algebra, is computationally unfeasible. We give an algorithm for obtaining smaller algebras to check admissibility and a range of examples to demonstrate the advantages of this approach. 1 Introduction Rules and axioms are the building blocks of a logic. Axioms are the assumptions of the logic, whereas rules are used to derive new facts from previously derived facts. Rules are usually formulated as IF-THEN statements, e.g. “IF x is an integer and x is positive THEN x+1 is a natural number”. More generally, a rule is a set of premises followed by a conclusion. In logic, the premises and the conclusion are formulas. In algebra they are usually equations, as in the cancellation rule “IF x + y = x + z THEN y = z”. Axioms are rules without a premise and can be read as, e.g., “x + y = y + x always holds”. In algebra one often uses Σ to denote a finite set of equations and calles the rule “IF Σ THEN ϕ ≈ ψ”, written Σ ⇒ ϕ ≈ ψ, a quasiequation. A quasiequation Σ ⇒ ϕ ≈ ψ is called valid in the finite algebra A if whenever every equation in Σ is true in A for a specific choice of elements of A for the variables occuring in Σ ∪ {ϕ ≈ ψ}, then also ϕ ≈ ψ is true in A for this choice. Checking validity in finite algebras (similarly, derivability in finite-valued logics) has been studied extensively in the literature, and may be considered a “solved problem” in the sense that there exist both general methods for obtaining proof systems for checking validity (tableaux, resolution, multisequents, etc.) and standard optimization techniques for such systems (lemma generation, indexing, etc.) (see, e.g., [1, 12, 24]). A rule which can be added to a given system without producing new valid equations is called admissible. This notion was introduced by Lorenzen in 1955 [18], but the property of being admissible was already used by Gentzen twenty years earlier [7]. Admissibility has been studied intensively in the context of intermediate and transitive modal logics and their algebras [6, 8, 9, 13, 15, 21], leading also to proof systems for checking admissibility [2, 10, 14], and certain many-valued logics and their algebras [5, 16, 17, 19, 21], but a general theory for this latter case has so far been lacking. Showing the admissibility of rules can play an important role in establishing com- pleteness results. That means for example, that one proves the admissibility of the cut-rule “IF x = y and y = z THEN x = z” to show that the system can derive the same equations without the cut-rule. Moreover, in some cases adding admissible rules to a system can simplify or speed up reasoning in this system. ✯ Supported by Swiss National Science Foundation grant 20002 129507. R.K. Rendsvig and S. Katrenko (Eds.): ESSLLI 2012 Student Session Proceedings, CEUR Work- shop Proceedings vol.: see http://ceur-ws.org/, 2012, pp. 133–141. 134 Christoph Röthlisberger Often it is possible to transform logical settings to algebraic settings and vice versa (see, e.g., [3]). In this sense rules and logics correspond to quasiequations and classes of algebras satisfying the same quasiequations, respectively. In this work we concentrate on the question, whether a given quasiequation is admissible in a finite algebra. This corresponds to the question, whether the quasiequation holds in a corresponding free algebra on countably infinitely many generators. Although it is well known that admis- sibility is decidable in finite algebras, the naive approach is computationally unfeasible. We give an algorithm to answer this question in a more efficient way. This paper (based on joint research with my supervisor [20]) focuses on proce- dural aspects of the given problem and its solution. Necessary algebraic definitions are provided, so that also readers without experience in universal algebra are able to understand the text. 2 Validity and Admissibility Let us first recall some basics from universal algebra. A language is a set of operation symbols L such that to each operation symbol f ∈ L a nonnegative integer ar(f ) is as- signed called the arity of f . An L-algebra A is an ordered pair A = hA, {f1A , . . . , fkA }i such that A is a set, called the universe of A, and each fiA is an operation on A, corre- sponding to an operation symbol fi ∈ L. We often omit superscripts when describing the operations of an algebra. Let A and B be two algebras of the same language. Then B is a subalgebra of A, written B ≤ A, if B ⊆ A and every operation of B is the restriction of the corresponding operation of A. For {a1 , . . . , ak } ⊆ A the smallest subalgebra of A containing {a1 , . . . , ak } is denoted by ha1 , . . . , ak i. We use the letters x, y, z, possibly indexed, to denote variables. Example 1. Let L = {→, e} be a language with ar(→) = 2 and ar(e) = 0. Define the algebra S→e 4 = h{−2, −1, 1, 2}, →, ei with the operations ( max{−x, y} x ≤ y x→y= and e = 1. min{−x, y} otherwise The algebra S→e 2 = h{−1, 1}, →, ei is a subalgebra of S→e →e 4 , i.e., S2 ≤ S→e 4 . Example 2. Let L consist of one operation symbol ⋆ with arity 1. Then consider the algebra P = h{a, b, c, d}, ⋆i where the unary operation ⋆ is described by the diagram below. The algebra h{a, b, d}, ⋆i is then clearly a subalgebra of P. P a b c d The set TmL of L-terms is inductively defined: every variable is an L-term and if ϕ1 , . . . , ϕn are L-terms and the operation symbol f ∈ L has arity n, then also f (ϕ1 , . . . , ϕn ) is an L-term. We denote the term algebra over countably infinitely Checking Admissibility in Finite Algebras 135 many variables by TmL (i.e., for each f ∈ L with ar(f ) = n, ϕ1 , . . . , ϕn ∈ TmL , f TmL (ϕ1 , . . . , ϕn ) is just the L-term f (ϕ1 , . . . , ϕn )) and let ϕ, ψ stand for arbitrary members of the universe TmL . An L-equation is a pair of L-terms, written ϕ ≈ ψ. If Σ is a finite set of L-equations, we call Σ ⇒ ϕ ≈ ψ an L-quasiequation. As usual, if the language is clear from the context we may omit the prefix L. Example 3. Terms in the language of Example 1 are, e.g., x, x → x or (x → e) → y whereas terms corresponding to Example 2 have the form ⋆(x) or ⋆(⋆(⋆(y))). The following is a quasiequation in the language of Example 1 {x ≈ y → x, x → e ≈ y} ⇒ x ≈ e. A homomorphism h between two algebras A and B of the same language L is a map h : A → B between their universes that preserves all the operations, i.e., for all a1 , . . . , an ∈ A and every operation f ∈ L with ar(f ) = n, h(f A (a1 , . . . , an )) = f B (h(a1 ), . . . , h(an )). The homomorphism h : A → B is called surjective if for all b ∈ B, there exists an a ∈ A such that h(a) = b. Two algebras A and B are said to be isomorphic, if there exists a surjective homomorphism h : A → B with h(a) 6= h(b) for all a 6= b. The algebra C with the universe C = {h(a) : a ∈ A} ⊆ B and the restrictions of the operations of B to C as operations is called a homomorphic image of A, written C ∈ H(A). We say that the quasiequation Σ ⇒ ϕ ≈ ψ is valid in A or “holds in A”, written Σ |=A ϕ ≈ ψ, if for every homomorphism h : TmL → A, h(ϕ′ ) = h(ψ ′ ) for all ϕ′ ≈ ψ ′ ∈ Σ implies h(ϕ) = h(ψ). Example 4. The quasiequation of Example 3 is not valid in S→e 4 since the homomor- phism h : TmL → S→e4 with h(x) = −1 and h(y) = 1 satisfies h(x) = h(y → x) and h(x → e) = h(y), but not h(x) = h(e). We also need the well-known fact (see, e.g., [4]) that taking homomorphic images and subalgebras preserves equations and quasiequations, respectively. Lemma 1. Let A be an algebra and Σ ∪ {ϕ ≈ ψ} a finite set of equations. Then (a) |=A ϕ ≈ ψ implies |=B ϕ ≈ ψ for all B ∈ H(A). (b) Σ |=A ϕ ≈ ψ implies Σ |=B ϕ ≈ ψ for all B ≤ A. For a nonnegative integer m, let FA (m) denote the free algebra with m generators of the L-algebra A, i.e., the algebra of equivalence classes [ϕ] of L-terms ϕ containing at most m variables x1 , . . . , xm such that two terms ϕ and ψ belong to the same class if and only if |=A ϕ ≈ ψ. The free algebra of the algebra A has the same language as A and for L-terms ϕ1 , . . . , ϕn and the operation f with ar(f ) = n we have f FA (m) ([ϕ1 ], . . . , [ϕn ]) = [f A (ϕ1 , . . . , ϕn )]. Lemma 2 ([21], [4]). Let A be a finite L-algebra and Σ ∪ {ϕ ≈ ψ} a finite set of L-equations. Then (a) FA (m) is finite for all m ∈ N. (b) |=FA (|A|) ϕ ≈ ψ if and only if |=A ϕ ≈ ψ. (c) Σ |=FA (|A|) ϕ ≈ ψ if and only if Σ |=FA (k) ϕ ≈ ψ, |A| ≤ k ∈ N. 136 Christoph Röthlisberger Intuitively an L-quasiequation Σ ⇒ ϕ ≈ ψ is admissible in an L-algebra A, if every substitution (i.e., every homomorphism from the term algebra to the term algebra), that makes every equation of Σ hold in A, also makes ϕ ≈ ψ hold in A. More formally, an L-quasiequation Σ ⇒ ϕ ≈ ψ is called admissible in A, if for every homomorphism σ : TmL → TmL : |=A σ(ϕ′ ) ≈ σ(ψ ′ ) for all ϕ′ ≈ ψ ′ ∈ Σ implies |=A σ(ϕ) ≈ σ(ψ). Quasiequations admissible in the n-element algebra A are, equivalently, quasiequations valid in FA (n). Lemma 3 ([19]). Σ ⇒ ϕ ≈ ψ is admissible in A iff Σ |=FA (|A|) ϕ ≈ ψ. If a quasiequation Σ ⇒ ϕ ≈ ψ is valid in an algebra A, then it is also admissible in A. However, the other direction is not true in general. We say that A is structurally complete, if admissibility and validity coincide for A, i.e., Σ ⇒ ϕ ≈ ψ is admissible in A if and only if Σ |=A ϕ ≈ ψ. Example 5. Consider the two-valued Boolean algebra 2 = h{0, 1}, ∧, ∨, ¬, 1, 0i. Sup- pose that a {∧, ∨, ¬, 1, 0}-quasiequation Σ ⇒ ϕ ≈ ψ is not valid in 2, i.e., there exists a homomorphism h : TmL → 2 such that h(ϕ′ ) = h(ψ ′ ) for all ϕ′ ≈ ψ ′ ∈ Σ and h(ϕ) 6= h(ψ). Define the homomorphism σ : TmL → TmL by sending each variable x to 1, if h(x) = 1 and to 0, if h(x) = 0. It follows immediately that |=2 σ(ϕ′ ) ≈ σ(ψ ′ ) for all ϕ′ ≈ ψ ′ ∈ Σ, but 6|=2 σ(ϕ) ≈ σ(ψ). So Σ ⇒ ϕ ≈ ψ is not admissible in 2, hence 2 is structurally complete. 3 A Procedure to Check Admissibility To check if a given quasiequation Σ ⇒ ϕ ≈ ψ is admissible in a finite algebra A, it suffices by Lemma 3 to check whether the quasiequation is valid in the free algebra FA (|A|), which we know is always finite. The validity of quasiequations in finite algebras is well studied and decidable (see, e.g., [1, 12, 24]). However, even free algebras on a small number of generators can be very large. E.g., the free algebra FS→e 4 (2) has 453 elements, where S→e 4 is the algebra of Example 1. We therefore seek smaller algebras B such that, as for FA (|A|): Σ ⇒ ϕ ≈ ψ is admissible in A ⇐⇒ Σ |=B ϕ ≈ ψ. Proposition 1. Let A, B be L-algebras such that B is a subalgebra of FA (|A|) and A is a homomorphic image of B. Then Σ ⇒ ϕ ≈ ψ is admissible in A iff Σ |=B ϕ ≈ ψ. Proof. Let Σ ⇒ ϕ ≈ ψ be admissible in A. So Σ |=FA (|A|) ϕ ≈ ψ by Lemma 3 and then Σ |=B ϕ ≈ ψ by Lemma 1. For the other direction suppose that Σ |=B ϕ ≈ ψ and |=A σ(ϕ′ ) ≈ σ(ψ ′ ) for all ϕ′ ≈ ψ ′ ∈ Σ. Then |=FA (n) σ(ϕ′ ) ≈ σ(ψ ′ ) for all ϕ′ ≈ ψ ′ ∈ Σ by Lemma 2 and therefore |=B σ(ϕ′ ) ≈ σ(ψ ′ ) for all ϕ′ ≈ ψ ′ ∈ Σ by Lemma 1. But then |=B σ(ϕ) ≈ σ(ψ) and since A is a homomorphic image of B, |=A σ(ϕ) ≈ σ(ψ) by Lemma 1. ⊓ ⊔ Note that every subalgebra B of a subalgebra C of the free algebra FA (|A|), i.e., B ≤ C ≤ FA (|A|), is a subalgebra of FA (|A|). So since FA (m1 ) ≤ FA (m2 ) for all m1 ≤ m2 (see, e.g., [4]), we possibly do not need |A| generators. This suggests the following procedure when A is finite: Checking Admissibility in Finite Algebras 137 (i) Find the smallest free algebra FA (m) such that A ∈ H(FA (m)). (ii) Compute subalgebras B of FA (m), increasing in their size, and check for each whether A ∈ H(B). (iii) Derive a proof system for a smallest B with the properties of (ii). Steps (i) and (ii) of the procedure have been implemented using macros implemented for the Algebra Workbench [23]. Step (iii) can be implemented directly making use of a system such as MUltlog/MUltseq [11, 22]. We now give some explanation how to implement the first two steps of the proce- dure. For a given A, we want to find the smallest free algebra FA (m) (m ≤ |A|) such that A is a homomorphic image of FA (m). The idea is to calculate first FA (0) and to check whether A ∈ H(FA (0)). Stop if this is the case, otherwise calculate FA (1) and check whether A ∈ H(FA (1)) and so on. Suppose that, given a finite algebra A = h{a1 , . . . , an }, f1 , . . . , fk i, we want to calculate the elements of FA (m). Recall that the elements of the free algebra can be seen as equivalence classes of terms. Therefore we need to know all the terms that are definable using the given generators. To decide whether two terms ϕ and ψ are the same, i.e., |=A ϕ ≈ ψ, we would have to check all the possible homomorphisms h : TmL → A. So we simulate the truth table checking by storing the elements by sequences of elements of A. We represent the m generators of FA (m) by sequences hπi (ā1 ), . . . , πi (ānm )i where ā1 , . . . , ānm are the elements of Am and πi , i = 1, . . . , m the i-th projection-map from Am to A and collect them in a set G. Then we run the function DefinableTerms (see Fig. 1) to get the elements of FA (m), stored as sequences of length nm in the set F. function DefinableTerms(G, {f1 , . . . , fk }) F ←G repeat F0 ← F for all f ∈ {f1 , . . . , fk } do F ← F ∪ { hf (g1 ), . . . , f (gar(f ) )i : g1 , . . . , gar(f ) ∈ F } end for until F0 == F return F end function Fig. 1. Algorithm to generate all the definable terms, given a set of generators G Example 6. Suppose that we want to calculate the elements of the free algebra for the algebra P = h{a, b, c, d}, ⋆i defined in Example 2. We certainly need generators for the free algebra since P has no constants, i.e., no nullary operations. So the first step will be to calculate FP (1): our generator is the sequence (a, b, c, d). Running the func- tion DefinableTerms((a, b, c, d), {⋆}) gives us F = {(a, b, c, d), (b, a, b, b), (a, b, a, a)}. It is easy to see that there cannot be a surjective homomorphism from FP (1) to A since A has four elements. So we have to calculate the algebra FP (2) with generators (a, a, a, a, b, b, b, b, c, c, c, c, d, d, d, d) and (a, b, c, d, a, b, c, d, a, b, c, d, a, b, c, d), which will give us a six element algebra that fulfills the requirement of the homomorphism. 138 Christoph Röthlisberger The second step of the procedure requires us to calculate subalgebras of the free algebra, increasing in their size. We could, at least theoretically, check A ∈ H(B) for all B ≤ FA (m). But since we are interested in the smallest algebras with this property, we generate the subalgebras by increasing their size and always testing whether they satisfy the property. The principles for the calculation of subalgebras are those of DefinableTerms defined in Fig. 1. Using the generating elements as arguments for the operations, we increase the set of “reached” elements as long as we get new elements. We first calculate all the one-generated subalgebras of the free algebra FA (m), i.e., hϕi for ϕ ∈ FA (m) and store their sizes |hϕi|. Now we know that the size of the two-generated subalgebra hϕ1 , ϕ2 i of FA (m) is at least max{|hϕ1 i|, |hϕ2 i|}. Suppose that k = min{|hϕi| : ϕ ∈ FA (m)}. If there is more than one ϕ ∈ FA (m) with |hϕi| = k, then we generate all the algebras (increasing the number of gener- ators) hϕ1 , . . . , ϕr i with max{|t1 |, . . . , |tr |} ≤ k, again testing if there exists a sur- jective homomorphism to A and storing their sizes. We then proceed similarly for k′ = min{|hϕi| : ϕ ∈ FA (m), |hϕi| > k}. As soon as we find an algebra B with A ∈ H(B) we have an upper-bound for the size of the algebras to test (note that this upper-bound always exists since it cannot exceed the size of the free algebra FA (m)). However, we then have to continue until we know that every combination of generators will lead to a subalgebra B′ with B ≤ B′ . It is not hard to see that step (i) is sound and terminating since we use the op- erations of the generating algebra A to calculating new, finite sequences of elements m of A. So there are at most |A||A| sequences. The soundness of step (ii) is, similar to the previous step, given by the construction of the subalgebras and the used bounds of the cardinalities of the algebras. The algorithm terminates since there are only finitely many subalgebras of the free algebra. Example 7. Consider the algebra S→¬ 3 = h{−1, 0, 1}, →, ¬i, where → is defined as in Example 1 and ¬x = −x. Note that an equation of the form ϕ ≈ ϕ → ϕ holds in S→¬ 3 iff ϕ is a theorem of the {→, ¬}-fragment of the logic RM. Now, following our procedure, we obtain: (i) S→¬ 3 6∈ H(FS→¬3 (1)), but S→¬ 3 ∈ H(FS→¬ 3 (2)). (ii) FS→¬ 3 (2) has 264 elements and the smallest subalgebras B ≤ FS→¬ 3 (2) with S→¬ 3 ∈ H(B) have 6 elements. The fact that we first check the smaller subalgebras is useful here: We only had to check the 264 one-generated algebras, 15 two-generated and 3 three-generated algebras rather than all the 5134 possible subalgebras of FS→¬ 3 (2). Example 8. Small changes in the universe or language of an algebra can dramati- cally change the size and structure of its free algebra. Consider the algebra S→¬e 4 = h{−2, −1, 1, 2}, →, ¬, ei where → and ¬ are defined as in Example 7 and =1. Although ¯ this algebra is only slightly different to S→e 4 and S→¬ 3 of the Examples 1 and 7, the appropriate free algebra is much smaller and only needs one generator: (i) S→¬e 4 6∈ H(FS→¬e 4 (0)), but S→¬e 4 ∈ H(FS→¬e 4 (1)). (ii) FS→¬e 4 (1) has 18 elements and the smallest subalgebras B ≤ FS→¬e 4 (1) with S4→¬e ∈ H(B) have 6 elements. Example 9. In some cases, it is possible to establish structural completeness results for the algebra A using the described procedure. The smallest B ≤ FA (m) with A ∈ H(B) may be an isomorphic copy of A itself. In particular, known structural completeness results have been confirmed for Checking Admissibility in Finite Algebras 139 L→ 1 3 = h{0, 2 , 1}, →L i the 3-element Komori C-algebra B1 = h{0, 12 , 1}, min, max, ¬G i the 3-element Stone algebra G3 = h{0, 12 , 1}, min, max, →G i the 3-element positive Gödel algebra S→ 3 = h{−1, 0, 1}, →S i the 3-element implicational Sugihara monoid where x →L y = min(1, 1 − x + y), x →G y is y if x > y, otherwise 1, ¬G x = x →G 0, and →S is the operation → of S→¬ 3 from Example 7. A new structural completeness result has also been established for the psuedocomplemented distributive lattice B2 obtained by adding a top element to the 4-element Boolean algebra. Example 10. There are even cases where we do not need any generators for the free algebra since the constants alone suffice. Consider the 5-valued Post algebra P5 = h{0, 1, 2, 3, 4}, ∧, ∨,′ , 0, 1i where h{0, 1, 2, 3, 4}, ∧, ∨i builds a 5-chain with 0 < 4 < 3 < 2 < 1 and 0′ = 1, 1′ = 2, 2′ = 3, 3′ = 4, 4′ = 0. This algebra builds the algebraic counterpart to the Post logic P5 . Running our procedure we recognize that P5 is isomorphic to FP5 (0), i.e., P5 is also structurally complete. Example 11. Consider the algebra D4 = h{⊥, a, b, ⊤}, ∧, ∨, ¬, ⊥, ⊤i, called the 4-element De Morgan algebra, consisting of a distributive bounded lattice with an involutive negation defined as shown below and also its constant-free case called the 4-element De Morgan lattice DL4 = h{⊥, a, b, ⊤}, ∧, ∨, ¬i. ⊤ b a b b b b ⊥ Following our procedure, we obtain: (i) D4 6∈ H(FD4 (1)) and DL L 4 6∈ H(FDL (1)), but D4 ∈ H(FD4 (2)) and D4 ∈ H(FDL (2)). 4 4 (ii) FD4 (2) has 168 elements, FDL (2) has 166 elements and the smallest subalgebras 4 of the free algebras, for which D4 and DL 4 are homomorphic images, have 10 and 8 elements, respectively. Example 12. Similar results were also obtained in [19] for Kleene algebras and lat- tices generated by the 3-element chains C3 = h{⊤, a, ⊥}, ∧, ∨, ¬, ⊥, ⊤i and CL 3 = h{⊤, a, ⊥}, ∧, ∨, ¬i where ¬ swaps ⊥ and ⊤ and leaves a fixed. In both cases the small- est subalgebra of the free algebra, for which C3 and CL 3 are homomorphic images, is a 4-element chain. Example 13. Consider the 3-valued Lukasiewicz algebra L3 = h{0, 21 , 1}, →, ¬i with x → y = min(1, 1 − x + y) and ¬x = 1 − x. Following our procedure: (i) L3 6∈ H(FL3 (0)), but L3 ∈ H(FL3 (1)). 140 Christoph Röthlisberger A |A| Quasivariety Q(A) |Free algebra| |Output algebra| L3 3 algebras for L3 (Ex. 13) |FA (1)| = 12 6 B1 3 Stone algebras (Ex. 9) |FA (1)| = 6 3 C3 3 Kleene algebras (Ex. 12) |FA (1)| = 6 4 L→3 3 algebras for L→ 3 (Ex. 9) |FA (2)| = 40 3 CL 3 3 Kleene lattices (Ex. 12) |FA (2)| = 82 4 S→¬ 3 3 algebras for RM→¬ (Ex. 7) |FA (2)| = 264 6 S→3 3 algebras for RM→ (Ex. 9) |FA (2)| = 60 3 G3 3 algebras for G3 (Ex. 9) |FA (2)| = 18 3 DL 4 4 De Morgan lattices (Ex. 11) |FA (2)| = 166 8 D4 4 De Morgan algebras (Ex. 11) |FA (2)| = 168 10 P 4 Q(P) (Ex. 2) |FA (2)| = 6 6 S→¬e 4 4 Q(S→¬e 4 ) (Ex. 8) |FA (1)| = 18 6 B2 5 Q(B2 ) (Ex. 9) |FA (1)| = 7 5 P5 5 algebras for P5 (Ex. 10) |FA (0)| = 5 5 Table 1. Algebras for checking admissibility (ii) FL3 (1) has 12 elements and the smallest subalgebras B ≤ FL3 (1) with L3 ∈ H(B) have 6 elements. Note that our procedure does not necessarily find the smallest algebra B for check- ing admissibility in A. I.e., there may be an algebra C with C ≤ B and Σ ⇒ ϕ ≈ ψ is admissible in A ⇐⇒ Σ |=C ϕ ≈ ψ. Example 14. Following our procedure for the algebra P defined in Example 2: (i) P 6∈ H(FP (1)), but P ∈ H(FP (2)). (ii) FP (2) has 6 elements and the smallest subalgebra B ≤ FP (2) with P ∈ H(B) is FP (2) itself. However, P can be embedded into FP (1) × FP (1); that is, P is structurally complete (see, e.g., [5]). But this means that a quasiequation Σ ⇒ ϕ ≈ ψ is admissible in P iff Σ ⇒ ϕ ≈ ψ is valid in P. This last issue, but also possibilities of improving the given procedure for checking admissibility (e.g., ruling out symmetric cases of generators when calculating a free algebra) will be the subject of future work. The given examples for our procedure are summarized in Table 1. References 1. M. Baaz, C. G. Fermüller, and G. Salzer. Automated Deduction for Many-Valued Logics. In Handbook of Automated Reasoning, volume II, chapter 20, pages 1355– 1402. Elsevier Science B.V., 2001. 2. S. Babenyshev, V. Rybakov, R. A. Schmidt, and D. Tishkovsky. A Tableau Method for Checking Rule Admissibility in S4. In Proceedings of UNIF 2009, volume 262 of ENTCS, pages 17–32, 2010. Checking Admissibility in Finite Algebras 141 3. W. J. Blok and D. Pigozzi. Algebraizable Logics. Number 396 in Memoirs of the American Mathematical Society volume 77. American Mathematical Society, 1989. 4. S. Burris and H. P. Sankappanavar. A Course in Universal Algebra, volume 78 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1981. 5. P. Cintula and G. Metcalfe. Structural Completeness in Fuzzy Logics. Notre Dame Journal of Formal Logic, 50(2):153–183, 2009. 6. P. Cintula and G. Metcalfe. Admissible Rules in the implication-negation fragment of intuitionistic logic. Annals of Pure and Applied Logic, 162(10):162–171, 2010. 7. G. Gentzen. Untersuchungen über das Logische Schliessen. Math. Zeitschrift, 39:176–210,405–431, 1935. 8. S. Ghilardi. Unification in Intuitionistic Logic. Journal of Symbolic Logic, 64(2):859–880, 1999. 9. S. Ghilardi. Best Solving Modal Equations. Annals of Pure and Applied Logic, 102(3):184–198, 2000. 10. S. Ghilardi. A resolution/tableaux algorithm for projective approximations in IPC. Logic Journal of the IGPL, 10(3):227–241, 2002. 11. A. J. Gil and G. Salzer. Homepage of MUltseq. http://www.logic.at/multseq. 12. R. Hähnle. Automated Deduction in Multiple-Valued Logics. OUP, 1993. 13. R. Iemhoff. On the Admissible Rules of Intuitionistic Propositional Logic. Journal of Symbolic Logic, 66(1):281–294, 2001. 14. R. Iemhoff and G. Metcalfe. Proof Theory for Admissible Rules. Annals of Pure and Applied Logic, 159(1–2):171–186, 2009. 15. E. Jeřábek. Admissible Rules of Modal Logics. Journal of Logic and Computation, 15:411–431, 2005. 16. E. Jeřábek. Admissible rules of Lukasiewicz logic. Journal of Logic and Computa- tion, 20(2):425–447, 2010. 17. E. Jeřábek. Bases of admissible rules of Lukasiewicz logic. Journal of Logic and Computation, 20(6):1149–1163, 2010. 18. P. Lorenzen. Einführung in die operative Logik und Mathematik, volume 78 of Grundlehren der mathematischen Wissenschaften. Springer, 1955. 19. G. Metcalfe and C. Röthlisberger. Admissibility in De Morgan algebras. Soft Computing, to appear. 20. G. Metcalfe and C. Röthlisberger. Unifiability and Admissibility in Finite Algebras. In Proceedings of CiE 2012, volume 7318 of LNCS, pages 485–495. Springer, 2012. 21. V.V. Rybakov. Admissibility of Logical Inference Rules, volume 136 of Studies in Logic and the Foundations of Mathematics. Elsevier, Amsterdam, 1997. 22. G. Salzer. Homepage of MUltlog. http://www.logic.at/multlog. 23. M. Sprenger. Algebra Workbench. http://www.algebraworkbench.net. 24. R. Zach. Proof theory of finite-valued logics. Master’s thesis, Technische Univer- sität Wien, 1993.