We implement an algorithm for extracting appropriate collections of classic-like sound and complete tableaux rules for a large class of nite-valued logics. Its output consists of Isabelle theories.1
This note will report on the rst developments towards the implementation
of a fully automated system for the extraction of adequate proof-theoretical
counterparts for su ciently expressive logics characterized by way of a nite
set of nite-valued truth-tables. The underlying algorithm was rst described
in [
The survey paper [
Section 2, right below, recalls the relevant de nitions and results concerning many-valued logics as well as their homologous presentation in terms of bivalent semantics de ned by clauses of a certain format we call `gentzenian'. An algorithm for endowing any su ciently expressive nite-valued logic with an adequate bivalent semantics is exhibited and illustrated for the case of L3, the well-known 3-valued logic of Lukasiewicz.
The concepts concerning tableau systems in general and the particular results that allow one to transform any computable gentzenian semantics into a corresponding collection of tableau rules are illustrated in section 3, for the case of L3. 1 A snapshot of the corresponding code can be checked in http://tinyurl.com/5cakro.
Section 4 discusses our current implementation, carefully explaining its expected inputs and outputs, and again illustrates its functioning for the case of L3. Advantages and shortcomings of our system, in its present state of completion, as well as conclusions and some directions for future work are mentioned in section 5. 2
Given a denumerable set At of atoms and a nite family Cct = f c ij gj2J of connectives, where arity( c i ) = i, let S denote the term algebra freely generated j by Cct over At. Here, a semantics Sem for the algebra S will be given by any collection of mappings fxkV gk2K where dom(xkV ) = S and codom(xkV ) = Vk, and where each collection of truth-values Vk is partitioned into sets of designated values, Dk, and undesignated ones, Uk. The mappings xkV themselves may be called ( -valued) valuations, where = Card(Vk). A bivalent semantics is any semantics where Dk and Uk are singleton sets, for any k 2 K. For bivalent semantics, valuations are often called bivaluations.
The canonical notion of (single-conclusion) entailment j=Sem Pow(S) S induced by a semantics Sem is de ned by setting Sem ' i xkV (') 2 Dk whenever xkV ( ) Dk, for every xkV 2 Sem. The pair hS; j=Semi may be called a generic -valued logic, where = Maxk2K (Card(Vk)).
If one now xes the sets of truth-values V, D and U , and considers, for each connective c ij an interpretation ccij : Vi ! V, one may immediately build i from that an associated algebra of truth-values T V = hV; D; f ccj gj2J i (in the present paper, whenever there is no risk of confusion, we shall not di erentiate notationally between a connective symbol c and its interpretation cc). A truthfunctional semantics is then de ned by the collection of all homomorphisms of S into T V. In this paper, the shorter expression -valued logic will be used to qualify any generic -valued truth-functional logic, for some nite , where is the minimal value for which the mentioned logic can be given a truth-functional semantics characterizing the same associated notion of entailment.
The canonical notion of entailment of any given semantics, and in particular of any given truth-functional semantics, may be emulated by a bivalent semantics. Indeed, consider V2 = fT; F g and D2 = fT g, and consider the `binary print' of the algebraic truth-values produced by the total mapping t : V ! V2, de ned by t(v) = T i v 2 D. For any -valuation xV of a given semantics Sem, consider now the characteristic total function bx = t xV . Now, collect all such bivaluations bx's into a new semantics Sem(2), and note that Sem(2) ' i
Sem '. The standard 2-valued notion of inference of Classical Logic is
characterized indeed by a bivalent truth-functional semantics. In general, though, a
bivalent characterization of a logic with a -valued truth-functional semantics
explores the trade-o between the `algebraic perspective' of many-valuedness,
with its many `algebraic truth-values' and its semantic characterization in terms
of a set of homomorphisms, on the one hand, and the classic-inclined `logical
perspective', with its emphasis on characterizations based on 2 `logical values',
on the other hand (for more detailed discussions of this issue, check [
Our running example in this paper will involve Lukasiewicz's well-known 3-valued logic L3, characterized by the algebra of truth-values hf1; 12 ; 0g; f1g; f:; !;_; ^gi, where the interpretation of the unary negation connective : sets :v1 = 1 v1 and the interpretation of the binary implication connective ! sets (v1 ! v2) = Min(1; 1 v1 + v2). The binary symbols _ and ^ can be introduced as primitive interpreting them through (v1 _ v2) = Max(v1; v2) and (v1 ^v2) = Min(v1; v2), but they can also more simply be introduced by de nition just like in Classical Logic, setting _ d==ef ( ! ) ! and ^ d==ef :(: _: ). The binary print of an arbitrary atom of L3 and of its negation is illustrated in the table below.
v t(v) :v t(:v) 1 T 1 F 2 0 F
Given some nite-valued logic L based on a set of truth-values V, we say that L is functionally complete over V if any n-valued operation, for n = Card(V), may be de ned with the help of a suitable combination of its primitive operai tors f ccj gj2J . When L is not functionally complete from the start, we may consider Lfc as any functionally complete n-valued conservative extension of L. Given truth-values v1; v2 2 V, we say that they are separated, and we write v1]v2, in case v1 and v2 belong to di erent classes of truth-values, that is, in case either v1 2 D and v2 2 U , or v1 2 U and v2 2 D. Given a unary, primitive or de ned, connective s of a given truth-functional logic, with interpretation sb, we say that s separates v1 and v2 in case sb(v1)] sb(v2). Obviously, for any pair of truth-values of Lfc it is possible to nd or to de ne in the corresponding term algebra an appropriate separating connective s. When that separation can be done exclusively with the help of the original language of L, we say that V is e ectively separable and the logic L, in that case, will be considered to be su ciently expressive for our purposes. It should be noticed that the vast majority of the most well-known nite-valued logics enjoy this expressivity property.
Notice in particular, from Table 1, how the negation connective of L3 separates the two undesignated truth-values. Based on Table 1, one may in fact easily provide a unique identi cation to each of the 3 initial algebraic truth-values, by way of the following statements: v = 1 i t(v) = T v = 21 i t(v) = F and t(:v) = F v = 0 i t(v) = F and t(:v) = T (I) One can also use this separating connective s : u::u in order to provide a bivalent description of each of the operators of the language. Consider for instance the cases of A : vw:(v ! w) and B : vw::(v ! w) (that is, B is sA):
A 1 12 0 1 1 12 0 12 1 1 12 Let's write T : ' and F : ', respectively, as abbreviations for t(x(')) = T and t(x(')) = F . Then, the statement (II) may be described in bivalent form, with the help of (I), by writing:
T : :( ! ) i
In [
1 j : : : j b('1m) = wm1 & : : : & b('nmm ) = wmnm :(G) Here, wij 2 fT; F g, each 'ij is a formula of L, the symbol ) represents implication (and , shall represent bi-implication, abbreviating the conjunction of two clauses of the form (G)), the symbol & represents conjunction, and j represents disjunction. The (meta)logic governing these clauses is fol, First-Order Classical Logic. One may alternatively represent a clause of the form (G) as W1 k m V1 s nm (b('sk) = wks ).
With a slight notational change and using fol, one can see (III) as a description done in an abbreviated gentzenian format:
T : :( ! ) , T : & F :
& T : : F : ( ! ) , T :
T : F : & F : & F : & F : : & F : : & T : : & F : j j & T : : Following the above line of reasoning, it is also correct to write, for instance, the clause: (II) (III) (IV) (V)
According to the reductive algorithm described in [
j F : & F : ) ?
) Wd2D V1 m<n Card(D) wmdn : smn( )
) Wu2U V1 m<n Card(U) wmun : smn( )
for every 2 S, where smn is the unary (primitive or de ned) connective that
we use to separate the truth-values m and n, and wmvn = t(smn(v)).
3
Generic tableau systems for nite-valued logics are known at least since [
The basic idea, explained in [
T : :( ! )
F : ( ! )
(V)tab
T :
F :
To those rules corresponding to the truth-tables of the operators and the
separating connectives, one should also add rules corresponding to the extra
axioms (C1){(C4). In practical cases, however, axioms (C3) and (C4) can often be
proven from the remaining ones. Moreover, axiom (C2) expresses just the usual
closure condition on tableau branches. On the other hand, axiom (C1) gives rise
in general to the following `dual-cut' branching rule, for arbitrary :
All other de nitions and concepts concerning the construction of tableaux are
standard (check [
One might be worried, with good reason, that the unrestrained use of the branching rule may potentially make the corresponding tableaux non-analytic. We will discuss that in the conclusion. The tableau rules originated from the above procedure can naturally be used in order to prove theorems, check conjectures and suggest counter-models, but also, in the meta-theory, to formulate and prove derived rules that can be used to simplify the original presentation of the logic as originated by our algorithm. So, for instance, the above illustrated complex three-branching rule for F : ( ! ) can eventually be simpli ed into one of the following equivalent two-branching rules: (V )tab We used the functional programming language ML to automate the axiom extraction process. ML provides us, among other advantages, with an elegant and suggestive syntax, and a very handy compile-time type checking and type inference that guarantees that we never run into unexpected run-time problems with our program, once it is proved correct with respect to the speci cation.
The relevant inputs of our program include the detailed de nition of a nitevalued logic, such as the logic L3 presented in the previous sections, together with an appropriate set of separating connectives for that logic.
Here's an example of a input for the logic L3, presented above, where the functions CSym, CAri and CTab take a connective and return its symbol (for printing), arity and truth-table, respectively. A truth-table of a given connective c is represented as the list of all pairs ([x1; : : : ; xn], y) such that c (x1; : : : ; xn) = y. (* PROGRAM SIGNATURE *)
signature LOGIC = sig type cct val Values val Designated val Connectives val SeparatingD val SeparatingND val CSym val CAri (* EXAMPLE OF L3 *) datatype cct = Neg | Imp ["0", "1/2", "1"]; ["1"]; [Neg, Imp]; []; [Neg]; fun CSym Neg = "~"
| CSym Imp = "-->"; fun CAri Neg = 1 | CAri Imp = 2; val CTab fun CTab Neg = [ (["0"], "1"), (["1/2"], "1/2"), (["1"], "0") ] | CTab Imp = [ (["0", "0"], "1"), (["0", "1/2"], "1"), (["0", "1"], "1"), (["1/2", "0"], "1/2"), (...) (["1", "1"], "1") ] end;
To perform the extraction, our program rst generates a list of all necessary rules, as explained in section 2. val rulesList = [T "~(A0)",
T "~(~(A0))", F "~(A0)", F "~(~(A0))",
T "A0 --> A1", T "~(A0 --> A1)", F "A0 --> A1",
F "~(A0 --> A1)" ];
Next, the program converts each connective's truth-table, here given by the function CTab, into a table where each value is exchanged by its binary print. The binary print of a value is calculated based on the separating connectives given as input (SeparatingD for designated values and SeparatingND for undesignated values). For instance, for the case of the connective Neg, the clauses are the following: (* A0 *)
(* ~(A0) *) ([F "A0",T "~(A0)"], ([F "A0",F "~(A0)"], ([T "A0"], [T "~(A0)"]) [F "~(A0)",F "~(~(A0))"]) [F "~(A0)",T "~(~(A0))"])
Now, for each formula in the list of rules, a search is performed through all tables generated in the latter step, and all clauses in which the given formula appears on the right hand side are returned. The left hand side of these clauses represents the branches of the desired tableau rule. For instance, the rules for T:~A and F:~A are: (* T:~A *) (* F:~A *) ([ [F "A0",T "~(A0)"] ], ([ [F "A0",F "~(A0)"], [T "A0"] ], T "~(A0)") F "~(A0)")
The next steps include the calculus of axioms (C3) and (C4), and the printing of all de nitions, concrete syntax and rules into a text le containing the full theory ready to use in Isabelle. Isabelle, also written in ML, is a generic theorem-proving environment based on a higher-order meta-logic in which it is quite simple to create theories with rules and axioms for various kinds of deductive formalisms, and equally straightforward to de ne tacticals for the automation of routine tasks and to prove theorems about these systems.
For the case of L3, here is the corresponding theory produced as output by our program: local axioms ax0: ax1: ax2: ax3: ax4: imports Sequents begin typedecl a consts
Trueprop :: "(seq'=>seq') => prop" True :: o False :: o TR :: "a => o" FR :: "a => o" Neg :: "a => a" Imp :: "[a,a] => a" ("T:_" [20] 20) ("F:_" [20] 20) ("~ _" [40] 40) ("_-->_" [24,25] 25)
:: "(seq) => prop" ("[_]" 5) ML {* fun seqtab_tr c [s] = Const(c,dummyT) $ seq_tr s; fun seqtab_tr' c [s] = Const(c,dummyT) $ seq_tr' s; *} parse_translation {* [("@Trueprop", seqtab_tr "Trueprop")] *} print_translation {* [("Trueprop", seqtab_tr' "@Trueprop")] *} axC1: "[| [ $H, T:A ] ; [ $H, F:A ] |] ==> [$H]" axC21: "[ $H, T:A, $E, F:A, $G]" axC22: "[ $H, F:A, $E, T:A, $G]" axC3: "[| [ $H, T:A, $G ] |] ==> [ $H, T:A, $G ]" axC4: "[| [ $H, T:~(A), $G ] ; [ $H, F:~(A), $G ] |]
==> [ $H, F:A, $G ]" "[| [ $H, F:A0, T:~(A0), $G ] |] ==> [ $H, T:~(A0), $G ]" "[| [ $H, F:A0, F:~(A0), $G ] ; [ $H, T:A0, $G ] |]
==> [ $H, F:~(A0), $G ]" "[| [ $H, F:A0, F:~(A0), $G ] |] ==> [ $H, F:~(~(A0)), $G ]" "[| [ $H, T:A0, $G ] |] ==> [ $H, T:~(~(A0)), $G ]" "[| [ $H, F:A0, T:~(A0), F:A1, T:~(A1), $G ] ; [ $H, T:A0, T:A1, $G ] ; [ $H, F:A0, F:~(A0), T:A1, $G ] ; [ $H, F:A0, F:~(A0), F:A1, F:~(A1), $G ] ; [ $H, F:A0, T:~(A0), T:A1, $G ] ; [ $H, F:A0, T:~(A0), F:A1, F:~(A1), $G ] |] ==> [ $H, T:A0 --> A1, $G ]" In this theory, consts lists the formula constructors. TR :: "a => o" means that the constructor TR takes a formula (typed a) and returns a signed formula (typed o). We also extract from the logic received as input each constructor's name to use as syntactic sugar, as well as its associativity rules and priority order.
In the generated axioms corresponding to the tableau rules, T:X and F:X are (signed) formulas, $H and $E are sequences of such formulas (contexts) that are not directly involved in the rule, each sequence between square brackets represents a tableau branch, and a collection of branches is delimited by [| and |]. The symbol ==> denotes Isabelle's meta-implication. In Isabelle, the application of a rule means that is possible to achieve the goal (sequence on the right of the meta-implication) once it's possible to prove the hypotheses (sequences on the left of the meta-implication), which constitute the collection of new subgoals at each step. The branching rule corresponds to axiom axC1, and the closure rule for a branch of the tableau corresponds to the axioms axC21 and axC22.
Note for instance that ax5 corresponds to rule (V)tab from the last section. The simpler rule (V )tab, mentioned in the same section, can of course be written in Isabelle as: ax5SS: "[| [ $H, T:A0, F:A1, $E ] ; [ $H, F:~(A0), T:~(A1), $E ] |]
==> [$H, F:A0 --> A1, $E]"
The proof that ax5 and ax5S are indeed equivalent tableau rules, i.e., that one
can derive one from the other in the presence of the remaining rules of our theory,
can now be done directly with the help of Isabelle's meta-logic. One might
notice that, while in [
There still remains some room for improvement and extension of both our algorithm (which should still, for instance, be upgraded in order to deal in general with rst-order truth-functional logics) and its implementation. By way of an example, we have assumed from the start that the logics received as inputs to our program came together with a suitable collection of separating connectives. This second input, however, could be dispensed with, as the set of all de nable unary connectives can in fact be automatically generated in nite time from any given initial set of operators of the input logic. That generation, however, may be costly for logics with a large number of truth-values and is not as yet performed by our system. Another direction that must be better explored, from the theoretical perspective, concerns the conditions for the admissibility or at least for the explicit control of the application of the dual-cut branching rule. On the one hand, the elimination of dual-cut has an obvious favorable e ect on the de nition of completely automated theorem-proving tacticals for our logics. If that result cannot be obtained in general but if we can at least guarantee, on the other hand, that this branching rule will never be needed, in each case, for more than a nite number of known formulas |say, the ones related to the original goal as constituting its subformulas or being the result of applying the separating connectives to its subformulas| then again this will make it possible to devise tacticals for obtaining fully automated derivations using the above described tableaux for our nite-valued logics.