Dev

examples/prop_satisfiables.txt

@@ -0,0 +1,4 @@
+X
+Y
+X&Y
+X|Y

examples/prop_tautologies.txt

@@ -0,0 +1,46 @@
+%% Tautologies from:
+%%   Melvin Fitting. "First-Order Logic and Automated Theorem Proving".
+
+%% from Tableaux exercises
+((P -> Q) & (Q -> R)) -> -(-R & P)
+(-P -> Q) -> ((P -> Q) -> Q)
+((P -> Q) -> P) -> P
+-(-(P & P) & P)
+--(-(P | Q) | (P | Q))
+-(-P | -Q) <- --(P & Q)
+((((A -> B) -> (-C -> -D)) -> C) -> E) -> ((E -> A) -> (D -> A))
+-(-(P & -(Q & R)) & -(-(P & -(R & P)) & -(-(S & Q) & -(-(P & S) & -(P & S)))))
+-(-(P & -(Q & R)) & -(-(-(S & R) & -(-(P & S) & -(P & S))) & -(P & -(P & Q))))
+
+%% from Resolution example
+((P & Q) | (R -> S)) -> ((P | (R -> S)) & (Q | (R -> S)))
+
+%% Hilbert System Axioms
+X -> (Y -> X)
+(X -> (Y -> Z)) -> ((X -> Y) -> (X -> Z))
+F -> X
+X -> T
+--X -> X
+X -> (-X -> Y)
+% axiom scheme 7 application
+(A & B) -> A
+% axiom scheme 8 application
+(A & B) -> B
+% axiom scheme 9 application
+(A -> X) -> ((B -> X) -> ((A | B) -> X))
+
+%% from Natural Deduction exercises
+% X -> (Y -> X)
+(X -> (Y -> Z)) -> ((X -> Y) -> (X -> Z))
+(-Y -> -X) -> ((-Y -> X) -> Y)
+% ((X -> Y) -> X) -> X
+(X & (Y | Z)) -> ((X & Y) | (X & Z))
+(X -> Y) -> (-(Y | Z) -> -(X | Z))
+-(-(P & P) & P)
+--(-(P | Q) | (P | Q))
+-(-P | -Q) <- --(P & Q)
+
+%% from Davis-Putnam exercises
+((P -> Q) -> (P -> R)) -> (P -> (Q -> R))
+(P & Q) <-> -(-P | -Q)
+(P -> Q) | (Q -> R)

pylogic/gui/gui.py

@@ -1,6 +1,7 @@
 import sys
 import string
 import os.path  # for file checks
+import time
 
 from PyQt4.QtCore import Qt, SIGNAL
 from PyQt4.QtGui import *
@@ -30,6 +31,18 @@ def appendOutput(self, string=""):
         outputBox.write(string)
 
 
+    def execute(self, func):
+         check_box = self.ui.checkBoxExecutionTime.isChecked()
+         start = 0
+         if check_box:
+             start = time.time()
+         output = func()
+         if check_box:
+             execution_time = time.time() - start
+             self.appendOutput("Execution time: " + execution_time.__str__())
+         return output
+
+
     def showAboutBox(self):
         aboutBox = MyAboutBox()
         aboutBox.setModal(False)
@@ -67,20 +80,23 @@ def propositionalCheck(self):
     def propositionalNNF(self):
         """Transform the current formula in input in NNF"""
         formula = propositional_parser.parse(self.getInputString())
-        output = formula.nnf()
+        func = lambda: formula.nnf()
+        output = self.execute(func)
         self.appendOutput(output.__str__())
 
     def propositionalCNF(self):
         """Transform the current formula in input in CNF"""
         formula = propositional_parser.parse(self.getInputString())
-        output = formula.cnf()
+        func = lambda: formula.cnf()
+        output = self.execute(func)
         self.appendOutput(output.__str__())
 
     def propositionalResolution(self):
         """Test if the current formula is a tautology, using the resolution
         method"""
         formula = propositional_parser.parse(self.getInputString())
-        output = propositional_resolution.is_tautology(formula)
+        func = lambda: propositional_resolution.is_tautology(formula)
+        output = self.execute(func)
         self.appendOutput("%s: %s" % (str(formula), output.__str__()) )
 
 

pylogic/gui/mainwindow.ui

@@ -158,6 +158,19 @@
            </property>
           </spacer>
          </item>
+         <item>
+          <widget class="QCheckBox" name="checkBoxExecutionTime">
+           <property name="enabled">
+            <bool>true</bool>
+           </property>
+           <property name="text">
+            <string>execution time</string>
+           </property>
+           <property name="checked">
+            <bool>true</bool>
+           </property>
+          </widget>
+         </item>
         </layout>
        </widget>
        <widget class="QWidget" name="tabFirstOrder">

pylogic/propositional/propositional_logic.py

@@ -36,6 +36,7 @@ def __init__(self, *args):
             connective = None
             subformula1 = letter
             subformula2 = None
+            depth = 0
         elif len(args) == 2:
             if args[0] != "not" and args[0] != logic.CONN["not"]:
                 raise Exception("Wrong connective: " + args[0])
@@ -44,6 +45,7 @@ def __init__(self, *args):
             connective = "not"
             subformula1 = args[1]
             subformula2 = None
+            depth = subformula1.depth + 1
         else:
             if args[0] in list(set(logic.CONN.values()) - set("!")):
                 connective = [ item[0]
@@ -61,10 +63,13 @@ def __init__(self, *args):
                 raise Exception("Wrong formula: " + args[2])
             subformula1 = args[1]
             subformula2 = args[2]
+            depth = max(subformula1.depth, subformula2.depth)
+            depth = depth + 1
 
         self.connective = connective
         self.subformula1 = subformula1
         self.subformula2 = subformula2
+        self.depth = depth
 
 
     def __str__(self):
@@ -83,6 +88,8 @@ def __eq__(self, other):
             return False
         if self.connective == None and other.connective == None:
             return self.subformula1 == other.subformula1
+        if self.depth != other.depth:
+            return False
         else:
             return self.connective == other.connective \
                 and self.subformula1 == other.subformula1 \
@@ -277,6 +284,42 @@ def __ne__(self, other):
         return not self.__eq__(other)
 
 
+    def __len__(self):
+        return len(self.list)
+
+
+    def equivalent(self, other):
+        """Check if two generalizations have the same elements independently of
+        their order"""
+        if self.connective != other.connective:
+            return False
+        if len(self.list) != len(other.list):
+            return False
+        other_list = list(other.list)
+        try:
+            for formula in self.list:
+                other_list.remove(formula)
+        except ValueError:
+            return False
+        return not other_list
+
+
+    def subsume(self, other):
+        """Check if the current generalization subsumes the 'other'
+        generalization"""
+        if self.connective != other.connective:
+            return False
+        if len(self.list) > len(other.list):
+            return False
+        other_list = list(other.list)
+        try:
+            for formula in self.list:
+                other_list.remove(formula)
+        except ValueError:
+            return False
+        return True
+
+
     def has_non_literal(self):
         """Check if in the list of formulas there are non-literal formulas."""
         if len(self.list) == 0: