In this paper we propose a Logic Calculator with three operation modes: evaluation of logical formulae; logical entailment and conversion of a formula to Disjunctive Normal Form (DNF) and Conjunctive Normal Form (CNF). It is worth noting there are no existing automated tools for these three computations integrated into one tool providing a graphical calculator format. Logic Calculator is available at https://sourceforge.net/p/logiccalculator.
In this paper we describe a helpful tool developed for the automatic computation of logic operations: the Logic Calculator. We show the development of the calculator and describe its functionality: (i) Evaluation of logical formulae. In this mode, it evaluates the basic Boolean operations: negation; conjunction; disjunction; conditional and bi-conditional. The user can insert the logical formula and the Logic Calculator displays the truth table along with the models of the formula. (ii) Logical entailment. In this mode, the user can insert a number of premises followed by a number of conclusions, so the Logic Calculator displays the truth table of each premise/conclusion and the result of whether or not these premises logically entail the given conclusions. (iii) Conversion to Disjunctive Normal Form (DNF) and Conjunctive Normal Form (CNF). In this mode, the user inserts a logical formula and the Logic Calculator outputs its representation in both DNF and CNF. The main bene t of the Logic Calculator is the automatic evaluation of complex logic operations where manual calculations may be too di cult and take a considerable time, while there may also be a lack of con dence concerning the logic results obtained by hand.
In this paper we consider the language L of propositional logic formed from the nite set of P24 = fa; b; : : : ; t; w; x; y; zg variables, where 24 denotes the maximum available number of variables in the Logic Calculator.
The set = f:; ^; _; !; $g denotes valid logical operators.
A Well Formed Formula (WFF), also called formula or sentence, is a
propositional formula containing a subset of variables from P24 and a subset of
operators from . Parentheses are used in the traditional way [
We can de ne a WFF as follows: { An atomic formula (atom or variable) is a formula. { If is a formula, then : is a formula. { If and are formulas, and is a binary connective, then
Where 2 n f:g is a binary connectives. is a formula.
A truth table is a list of all possible truth assignments (possible worlds) for
the set of variables. Such a table typically contains several rows and columns,
with the header representing the variables and the WFF. The truth table is
composed of one column for each input variable and one nal column for all possible
results of the logical operation that the table represents [
A model of a propositional formula is a possible interpretation where is true under the interpretation in the classical truth functional manner. If there is a model for , then is said to be satis able.
When we want to know whether a set of sentences is a logical conclusion of
another set of sentences, this is known as logical entailment [
A literal is an atom or negation of an atom. A formula is in Conjunctive
Normal Form (CNF) if it is a conjunction of clauses, where a clause is a
disjunction of literals. A formula is in Disjunctive Normal Form (DNF) if it is a
disjunction of terms, where a term is a conjunction of literals. As in CNF, the
only propositional operators in DNF are ^, _, and :. The : operator can only
appear as part of a literal, which means that it can only precede an atom [
In this section we describe the modules and functionality of the Logic Calculator. We explain the main algorithms implemented and show some examples of using the three Logic Calculator modes. 3.1
The rst mode developed was the evaluation of logical formulae, since this is the basic functionality and is also used by the Logical entailment mode.
The rst step is to translate the input in x formula into a Reverse Polish
Notation (RPN) (post x notation) using the Algorithm 1, based on Dijkstra's
Shunting-yard algorithm [
Algorithm 1: Shunting-yard algorithm adapted for logical operators.
input : WFF output: RPN WFF 1 foreach token in turn in the input WFF do 2 if token is a variable 2 P24 then 3 Append to the post x output 4 else if token is `(' then 5 push `(' onto the stack 6 else if token is an operator 7 while there is an operator the stack do
Pop o the stack Append to the post x output 2 then
of higher or equal precedence than end
Push onto the stack else if token is `)' then repeat
Pop token x o the stack if x 2 then
Append x to the post x output
To parse the expression, the operator precedence must also be de ned. The
list of valid operators in order of precedence (highest to lowest) is: [
For example, the WFF 1 is processed by Algorithm 1, producing the RPN WFF 2.
p _ q $ (q ! r) ^ :s p q _ q r ! s : ^ $ (1) (2)
The second step consists in setting up the truth table for the formula variables. If we consider the case where n is the number of distinct variables in the formula, then we need to set up a truth table with n columns and 2n rows, as follows: column under the rst variable should alternate 2n 1 true's with 2n 1 false's; column under the second variable should alternate 2n 2 true's with 2n 2 false's; continuing until we reach the last column variable.
The third step consists of evaluating the RPN WFF for each interpretation of the generated truth table. The explicitness of the RPN WFF obtained by Algorithm 1 allows us to implement the algorithm for evaluating post x notation in a straightforward manner. Algorithm 2 shows the RPN parser developed using a stack as a helper data structure.
For example given the RPN Formula 2 and the interpretation p = 1, q = 0, r = 1 and s = 0, Algorithm 2 outputs 1 as the result of the evaluation. There are 24 calls to Algorithm 2 since there are 4 variables in this formula. 3.2
In this mode we ca determine whether a set of premises logically entails a conclusion (or set of conclusions). The logical symbol j= allows us to represent a logical entailment, separating the premises from the conclusion, with associativity from left to right. Premises are separated by commas (;). Parentheses are used in the classical way, usually to override the normal precedence of operators. Premises and conclusions are WFFs.
First step is to save the premises in a list and store the conclusion in separate lists. After evaluating each WFF from the premises part (using the modules developed for the Logical formula evaluator mode) and evaluating each WFF from the conclusion, a nal truth table is used to determine whether the logical entailment holds (see Algorithm 3).
Algorithm 3: Logical entailment processor.
input : Premises list, conclusions list output: Whether logical entailment holds 1 foreach WFF in premises list do 2 Evaluate truth table of 3 Add truth table to nal table 4 end 5 foreach WFF in conclusions list do 6 Evaluate truth table of 7 Add truth table to nal table 8 end 9 Evaluate
For example, given the following case: p _ q; q ! r; :s j= q _ r (3)
We have the problem of determining whether fq _ rg (the conclusion) is logically entailed from fp _ q; q ! r; :sg (the premises). So, the Logic Calculator prints the nal truth table and the result, in this case: \Premises do not logically entail the conclusion". 3.3
The conversion of a WFF to its DNF and CNF is made in two steps. First, a binary tree is created from parsing the WFF. Operator ! is used to build the tree from the minor priority operator. For example, the binary tree shown in Figure 1 is created from Formula 4 with respect to the priority of operators. a ! b ^ c _ d ! e (4)
Second, the WFF conversion to CNF (resp. DNF) is based on the laws
governing CNF and DNF conversion [
For example, walking through the binary tree t and generating the tree shown in Figure 2, resulting in the CNF shown in Formula 5. Similarly, the tree shown in Figure 3 corresponds to the DNF formula shown in Formula 6. :b :c
^ _
_ e :d e a
_ ^
^ :b :d
_ a ^
^ :c :d e (a ^ :b ^ :d) _ (a ^ :c ^ :d) _ e (5) (6)
It is worth clarifying that the Logic Calculator converts to an equivalent
CNF formula rather than an equisatis able CNF formula (via the insertion of
new variables [
One of the goals of the Logic Calculator is to provide a user-friendly User Interface (UI) similar to an arithmetic calculator. Figure 4 shows the GUI of the Logic Calculator in Logical formula evaluator mode. The output box is a text area for convenience, allowing easy copying and pasting of formulae. Debug area outputs debug details and log information. 4
We stress-tested the Logic Calculator on an Alienware M17x laptop, with an Intel Core i7-2670QM CPU @2.20GHz 8, 8 GB in RAM, 500 GB in HDD, Ubuntu Linux 12.04 64-bit and OpenJDK 7 64-bit.
Table 1 (column Op1) shows processing time plus printing time of the truth table. Memory is an issue when printing a truth table of 23 variables because 223 = 8388608 interpretations, so the Logic Calculator runs out of memory at printing 4206949 lines. This runtime exception is thrown depending on the amount of virtual memory that the JVM has access to. But we can perform operations with up to 24 variables without memory problems. For example, Table 1 (column Op2) shows processing time but only printing the number of models without printing the truth table, and Table 1 (column Op3) shows time performing conversions of WFF to their CNF and DNF. We can see that computing formulae conversions is quite quick, even for 24 variables formula.
The main bene t of the Logic Calculator is the automatic evaluation of complex logic operations. For example, to evaluate complex logical formulae with at most 24 variables and any number of parentheses, or to determine if a set of highly elaborate premises logically entails a set of highly elaborate conclusions, or to translate complex logical formulae to CNF or DNF, are highly complex tasks. Currently there are no tools which can solve these problems e ectively, in a userfriend manner. Logic Calculator addresses these issues, so it can be an e ective tool for new methods of reasoning.
The Logic Calculator was developed under the Open Java Development Kit
(OpenJDK) 7 but source code using Java 5 as target, therefore it needs Java
Runtime Environment version 5 or higher. OpenJDK platform has the same
attributes of the o cial JDK, plus the bene ts of being free software [
Multiplatform support is also an advantage, thus it can be executed over recent versions of Microsoft Windows, most Linux distributions, most UNIX variants and modern versions of Mac OS. Future work considers improve the e ciency of algorithms, manage more variables and a possible implementation in a hardware device.
Logic Calculator source code is downloadable from Sourceforge repositories at https://sourceforge.net/p/logiccalculator. A number of downloads up to 2016 is available at https://sourceforge.net/projects/logiccalculator/ files/stats/timeline?dates=2013-09-27+to+2016-12-31.
To CONACYT for supporting the doctoral program in Computer Science at the Universidad Juarez Autonoma de Tabasco.