boolexman

boolean expression manipulator for educational purposes

boolexman is a boolean expression manipulator (program) to aid teaching or studying propositional logic, primarily aimed for the Informatics 1 - Computation and Logic at The University of Edinburgh School of Informatics.

boolexman offers various commands for working with boolean expressions, from those that can transform any given expression into Disjunctive Normal Form (i.e. an OR of ANDs) or Conjunctive Normal Form (i.e. an AND of ORs), to those (functions) for fully-automated resolution, entailment, and partial-evaluation. All commands shows their working step-by-step, with detailed explanations of each rule that was used.

Setup

Clone the repository

$ git clone https://github.com/boramalper/boolexman
$ cd boolexman

Update the cabal package cache
```
$ cabal update
```

Install the dependencies of boolexman:

$ cabal install --only-dependencies --enable-tests

Test if boolexman works:
```
$ cabal run
```
(Optional) Install it to your system:
```
$ cabal install
```
- If you wish not to install, you can always navigate to the directory you cloned boolexman to, and execute cabal run.

Running the Tests

Navigate to the directory you cloned boolexman to, and execute cabal test.

Beware that some of the tests might (very likely indeed) timeout -due to some performance problems I intend to address in an unforeseeable future- none of the tests should fail.

If you intend to contribute to boolexman, contact me at bora@boramalper.org.

Compiling the Web Application from the Sources

boolexman can be transmogrified into JavaScript, which in turn allows it to be used as a Web application in browser, all thanks to GHCJS. Although it might not be as reliable as the traditional method, it also makes boolexman significantly more affordable.

Install AND setup GHCJS, and all of its requirements by following the documentation:

https://github.com/ghcjs/ghcjs
- Booting (i.e. ghcjs-boot) might take a while, be patient.
Enter the src/ directory:
```
cd src/
```

Transmogrify boolexman:

ghcjs -main-is WebMain --make WebMain.hs -o boolexman

Copy the JavaScript files:

cp boolexman.jsexe/lib.js boolexman.jsexe/out.js boolexman.jsexe/rts.js boolexman.jsexe/runmain.js ../web/

(Optional) Get rid of the .js_hi and .js_o files:
```
rm -r *.js* Engine/*.js*
```

Quick Manual

Each time you run boolexman, you will be greeted with a screen like follows:

boolexman - boolean expression manipulator | v0.2.0.0

   1>

1> is called the prompt, and it indicates that boolexman is ready to accept your command. The number before the greater-than symbol shows the command number, which is provided only as a convenience to the user and has no importance to the program at all. boolexman uses Haskeline library to provide a GNU Readline-like rich line-editing functionality to its users, including moving backwards/forwards in the command history to Emacs/vi specific key bindings, whose full list can be found on Haskeline Wiki.

Every command consists of a verb (i.e. command verb), and arguments of some format, which depends on the verb but is consistent throughout the boolexman. Whilst any errors are printed on the prompt screen, the output of the commands are piped to the less, which allows you to scroll in all four directions (which is a crucial functionality since some commands produce large outputs [i.e. entailment trees]). You can also save the output of your commands to the disk, which are explained below.

Command Verbs

Every command to the boolexman must start with a command verb, followed by zero or more space-separated arguments. Every command verb starts with a letter, followed by optionally some more alphanumeric characters. Command verbs are case-insensitive!

quit

Quits the program. Takes no arguments.

symbols expression :: Expression

Extracts all the symbols of expression.

Example:

   1> symbols (if A iff not B then C implies D xor E else True and F or not D)

    1 symbols ((A <=> !B) ? (C => (D + E)) : ((True ^ F) v !D))
    2 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
    3
    4   • A
    5   • B
    6   • C
    7   • D
    8   • E
    9   • F

subexpressions expression :: Expression

Finds all the subexpressions of expression, including the expression itself.

Example:

   1> subexpressions (if A iff not B then C implies D xor E else True and F or not D)

    1 subexpressions ((A <=> !B) ? (C => (D + E)) : ((True ^ F) v !D))
    2 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
    3
    4 Sub-Expression Tree:
    5   ((A <=> !B) ? (C => (D + E)) : ((True ^ F) v !D))
    6   ├─ (A <=> !B)
    7   │  ├─ A
    8   │  ├─ !B
    9   │  │  ├─ B
   10   ├─ (C => (D + E))
   11   │  ├─ C
   12   │  ├─ (D + E)
   13   │  │  ├─ D
   14   │  │  ├─ E
   15   ├─ ((True ^ F) v !D)
   16   │  ├─ (True ^ F)
   17   │  │  ├─ True
   18   │  │  ├─ F
   19   │  ├─ !D
   20   │  │  ├─ D
   21
   22 Sub-Expression List:
   23   • True
   24   • A
   25   • B
   26   • C
   27   • D
   28   • E
   29   • F
   30   • !B
   31   • !D
   32   • (D + E)
   33   • (True ^ F)
   34   • (A <=> !B)
   35   • (C => (D + E))
   36   • ((True ^ F) v !D)
   37   • ((A <=> !B) ? (C => (D + E)) : ((True ^ F) v !D))

tabulate expression :: Expression

Constructs a truth table with subexpressions as columns, and possible evaluations as rows of the truth table.

Example:

   1> tabulate (C implies D xor E <=> True and F or not D)

    1 tabulate ((C => (D + E)) <=> ((True ^ F) v !D))
    2 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
    3
    4 ╔════╤═╤═╤═╤═╤══╤═══════╤══════════╤══════════════╤═════════════════╤══════════════════════════════════════╗
    5 ║True│C│D│E│F│!D│(D + E)│(True ^ F)│(C => (D + E))│((True ^ F) v !D)│((C => (D + E)) <=> ((True ^ F) v !D))║
    6 ╟────┼─┼─┼─┼─┼──┼───────┼──────────┼──────────────┼─────────────────┼──────────────────────────────────────╢
    7 ║ T  │F│F│F│F│T │   F   │    F     │      T       │        T        │                  T                   ║
    8 ║ T  │F│F│F│T│T │   F   │    T     │      T       │        T        │                  T                   ║
    9 ║ T  │F│F│T│F│T │   T   │    F     │      T       │        T        │                  T                   ║
   10 ║ T  │F│F│T│T│T │   T   │    T     │      T       │        T        │                  T                   ║
   11 ║ T  │F│T│F│F│F │   T   │    F     │      T       │        F        │                  F                   ║
   12 ║ T  │F│T│F│T│F │   T   │    T     │      T       │        T        │                  T                   ║
   13 ║ T  │F│T│T│F│F │   F   │    F     │      T       │        F        │                  F                   ║
   14 ║ T  │F│T│T│T│F │   F   │    T     │      T       │        T        │                  T                   ║
   15 ║ T  │T│F│F│F│T │   F   │    F     │      F       │        T        │                  F                   ║
   16 ║ T  │T│F│F│T│T │   F   │    T     │      F       │        T        │                  F                   ║
   17 ║ T  │T│F│T│F│T │   T   │    F     │      T       │        T        │                  T                   ║
   18 ║ T  │T│F│T│T│T │   T   │    T     │      T       │        T        │                  T                   ║
   19 ║ T  │T│T│F│F│F │   T   │    F     │      T       │        F        │                  F                   ║
   20 ║ T  │T│T│F│T│F │   T   │    T     │      T       │        T        │                  T                   ║
   21 ║ T  │T│T│T│F│F │   F   │    F     │      F       │        F        │                  T                   ║
   22 ║ T  │T│T│T│T│F │   F   │    T     │      F       │        T        │                  F                   ║
   23 ╚════╧═╧═╧═╧═╧══╧═══════╧══════════╧══════════════╧═════════════════╧══════════════════════════════════════╝

eval symbols that are true :: List of Symbols symbols that are false :: List of Symbols expression :: Expression

Evaluates the expression given a set of symbols that are true and symbols that are false. If not every symbol in the expression appears in at least one of the sets, then the expression will be partially evaluated and the result will be in terms of those symbols that do not exists in neither set, in Disjunctive Normal Form.

If some symbols that do not appear in the expression appear in one of the list of symbols, boolexman will display a warning at the top of its output, but otherwise will work as intended.

If some symbols appear in both lists of symbols, then boolexman will display an error.

Example:

   1> eval [A, D] [E,Z] (if A iff not B then C implies D xor E else True and F or not D)

    1 eval [A,D] [E,Z] ((A <=> !B) ? (C => (D + E)) : ((True ^ F) v !D))
    2 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
    3
    4 WARNING: Some of the true/false symbols have not been found in the expression!
    5
    6   Redundant False Symbols: [Z]
    7
    8 1. Transform into Conjunctive Normal Form:
    9   • {F, !D, !A, !B}
   10   • {F, !D, B, A}
   11   • {A, !B, !C, D, E}
   12   • {A, !B, !C, !D, !E}
   13   • {!A, B, !C, D, E}
   14   • {!A, B, !C, !D, !E}
   15   • {F, !D, !C, !E}
   16
   17 2. Eliminate all maxterms which constains a true symbol:
   18   • {F, !D, B, A}
   19     is eliminated because A is true.
   20   • {A, !B, !C, D, E}
   21     is eliminated because A is true.
   22   • {A, !B, !C, !D, !E}
   23     is eliminated because A is true.
   24   • {!A, B, !C, D, E}
   25     is eliminated because D is true.
   26   • {!A, B, !C, !D, !E}
   27     is eliminated because !E is true.
   28   • {F, !D, !C, !E}
   29     is eliminated because !E is true.
   30
   31 Remaining maxterms:
   32   • {F, !D, !A, !B}
   33
   34 3. Transform into Disjunctive Normal Form:
   35   • {F, !D, !A, !B}
   36
   37 4. Eliminate all minterms which constains a false symbol:
   38   • {F, !D, !A, !B}
   39     is eliminated because !A is false.
   40
   41 Remaining minterms:
   42   • {False}
   43
   44 Resultant expression:
   45   False

toCNF/toDNF expression :: Expression

Tranforms the expression into Disjunctive/Conjunctive Normal Form.

Example:

   1> toCNF (if A iff not B then C implies D else True and F or not D)

    1 toCNF ((A <=> !B) ? (C => D) : ((True ^ F) v !D))
    2 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
    3
    4 1. Transform all if-then-else (ITE) expressions:
    5   • ((A <=> !B) ? (C => D) : (F v !D))
    6     is transformed into
    7     (((A <=> !B) ^ (C => D)) v (!(A <=> !B) ^ (F v !D)))
    8
    9 After all ITE expressions are transformed:
   10   (((A <=> !B) ^ (C => D)) v (!(A <=> !B) ^ (F v !D)))
   11
   12 2. Transform all if-and-only-if (IFF) expressions:
   13   • (A <=> !B)
   14     is transformed into
   15     !(A + !B)
   16
   17 After all IFF expressions are transformed:
   18   ((!(A + !B) ^ (C => D)) v (!!(A + !B) ^ (F v !D)))
   19
   20 3. Tranform all implications:
   21   • (C => D)
   22     is transformed into
   23     (!C v D)
   24
   25 After all implications are transformed:
   26   ((!(A + !B) ^ (!C v D)) v (!!(A + !B) ^ (F v !D)))
   27
   28 4. Tranform all exclusive-or (XOR) expressions:
   29   • (A + !B)
   30     is transformed into
   31     ((A v !B) ^ (!A v !!B))
   32
   33 After all XOR expressions are transformed:
   34   ((!((A v !B) ^ (!A v !!B)) ^ (!C v D)) v (!!((A v !B) ^ (!A v !!B)) ^ (F v !D)))
   35
   36 5. Distribute NOTs:
   37   • !!B
   38     is transformed into
   39     B
   40   • !((A v !B) ^ (!A v B))
   41     is transformed into
   42     (!(A v !B) v !(!A v B))
   43   • !(A v !B)
   44     is transformed into
   45     (!A ^ !!B)
   46   • !(!A v B)
   47     is transformed into
   48     (!!A ^ !B)
   49   • !!A
   50     is transformed into
   51     A
   52   • !((!A ^ B) v (A ^ !B))
   53     is transformed into
   54     (!(!A ^ B) ^ !(A ^ !B))
   55   • !(!A ^ B)
   56     is transformed into
   57     (!!A v !B)
   58   • !(A ^ !B)
   59     is transformed into
   60     (!A v !!B)
   61
   62 After all NOTs are distributed:
   63   ((((!A ^ B) v (A ^ !B)) ^ (!C v D)) v ((A v !B) ^ (!A v B) ^ (F v !D)))
   64
   65 6. Distribute ORs over ANDs:
   66   • ((!A ^ B) v (A ^ !B))
   67     is transformed into
   68     ((!A v !B) ^ (B v A))
   69   • (((!A v !B) ^ (B v A) ^ (!C v D)) v ((A v !B) ^ (!A v B) ^ (F v !D)))
   70     is transformed into
   71     ((((!A v !B) ^ (B v A)) v A v !B) ^ (((!A v !B) ^ (B v A)) v !A v B) ^ (((!A v !B) ^ (B v A)) v F v !D) ^ (!C v D v A v !B) ^ (!C v D v !A v B))
   72   • (((!A v !B) ^ (B v A)) v A v !B)
   73     is transformed into
   74     True
   75   • (((!A v !B) ^ (B v A)) v !A v B)
   76     is transformed into
   77     True
   78   • (((!A v !B) ^ (B v A)) v F v !D)
   79     is transformed into
   80     ((F v !D v !A v !B) ^ (F v !D v B v A))
   81
   82 Resultant expression:
   83   ((F v !D v !A v !B) ^ (F v !D v B v A) ^ (!C v D v A v !B) ^ (!C v D v !A v B))

resolve expression :: Expression

Iteratively applies the resolution rule to automatically resolve an expression until either an empty clause is found or there are no more symbols to resolve on left.

Example:

   1> resolve (if A iff not B then C implies D xor E else True and F or not D)

    1 resolve ((A <=> !B) ? (C => (D + E)) : ((True ^ F) v !D))
    2 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
    3
    4       • B[F,!D,!A,!B]
    5       • B[F,!D,B,A]
    6       • B[A,!B,!C,D,E]
    7       • B[A,!B,!C,!D,!E]
    8       • B[!A,B,!C,D,E]
    9       • B[!A,B,!C,!D,!E]
   10       • [F,!D,!C,!E]
   11     
   12   • ──┤ B ├────────────
   13       • ~[F,!D,A,!A]~
   14       • ~[F,!D,A,!C,D,E]~
   15       • A[F,!D,A,!C,!E]
   16       • ~[!A,!C,D,E,F,!D]~
   17       • ~[!A,!C,D,E,A]~
   18       • ~[!A,!C,D,E,A,!D,!E]~
   19       • A[!A,!C,!D,!E,F]
   20       • ~[!A,!C,!D,!E,A,D,E]~
   21       • ~[!A,!C,!D,!E,A]~
   22     
   23   • ──┤ A ├────────────
   24       • [F,!D,!C,!E]
   25

entail antecedent :: Expression consequent :: Expression

Automatically constructs a (Gentzen-style) sequent calculus tree that branches bottom-up.

Bugs:

boolexman requires both antecedent and consequent to be non empty (i.e. non ()) expressions. As a workaround, you can supply an expression that consists of a single symbol that does not appear in the other expression.

Example:

   1> entail (Q) (if A iff not B then C implies D xor E else F or not D)

    entail Q ((A <=> !B) ? (C => (D + E)) : (F v !D))
    ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━

    1(a). Transform all if-then-else (ITE) expressions in the condition:
      No ITE expressions are found in the condition!

    1(b). Transform all if-then-else (ITE) expressions in the consequence:
      • ((A <=> !B) ? (C => (D + E)) : (F v !D))
        is transformed into
        (((A <=> !B) ^ (C => (D + E))) v (!(A <=> !B) ^ (F v !D)))

    After all ITE expressions in the entailment are transformed:
      Q |- (((A <=> !B) ^ (C => (D + E))) v (!(A <=> !B) ^ (F v !D)))

    2(a). Transform all if-and-only-if (IFF) expressions in the condition:
      No IFF expressions are found in the condition!

    2(b). Transform all if-and-only-if (IFF) expressions in the consequence:
      • (A <=> !B)
        is transformed into
        !(A + !B)
      • (A <=> !B)
        is transformed into
        !(A + !B)

    After all IFF expressions in the entailment are transformed:
      Q |- ((!(A + !B) ^ (C => (D + E))) v (!!(A + !B) ^ (F v !D)))

    3(a). Transform all exclusive-or (XOR) expressions in the condition:
      No XOR expressions are found in the condition!

    3(b). Transform all exclusive-or (XOR) expressions in the consequence:
      • (A + !B)
        is transformed into
        ((A v !B) ^ (!A v !!B))
      • (D + E)
        is transformed into
        ((D v E) ^ (!D v !E))
      • (A + !B)
        is transformed into
        ((A v !B) ^ (!A v !!B))

    After all XOR expressions in the entailment are transformed:
      Q |- ((!((A v !B) ^ (!A v !!B)) ^ (C => ((D v E) ^ (!D v !E)))) v (!!((A v !B) ^ (!A v !!B)) ^ (F v !D)))

                                                                                                                                                                                                                                                                                                                                                                                               ────────────────── (F)                                                                                                                                                               
                                                                                                                                                                                                                                                                                                                                                                                               A, E, D, C, Q |- B                                                                                                                                                                   
                                                                                                                                                                                                                                                                                                                                                                                               ────────────────────── (!L)                                                                                                                                                          
                                                                                                                                                                                                                                                                                                                                                                                               !B, A, E, D, C, Q |-                                                                                                                                                                 
                                                                                                                                                                                                                                                                                 ────────────────── (F)                                           ────────────────── (F)                       ─────────────────────────── (!R)                                                                                                                                                     
                                                                                                                                                                                                                                                                                 A, C, Q |- B, D, E                                               B, E, D, C, Q |- A                              A, E, D, C, Q |- !!B                                                                                                                                                              
                                                                                                                                                                                                                                                                                 ────────────────────── (!L)                                      ────────────────────── (!R)                  ──────────────────────────────── (!R)                                                                                                                                                
                                                                                                                                                                                                                                                                                  !B, A, C, Q |- D, E                                              E, D, C, Q |- A, !B                              E, D, C, Q |- !A, !!B                                                                                                                                                           
                                                                                                   ─────────────── (F)                       ─────────────── (F)                                                                              ────────────────── (F)             ─────────────────────────── (!R)                                 ─────────────────────────── (!R)             ───────────────────────────────────── (!R)                                                                                                                                           
                                                                                                   D, B, A, Q |- F                           D, Q |- B, A, F                                                                                  B, C, Q |- D, E, A                    A, C, Q |- D, E, !!B                                             D, C, Q |- !E, A, !B                             D, C, Q |- !E, !A, !!B                                                                                                                                                        
                                                                                                   ─────────────────── (!R)                  ─────────────────── (!R)                                                                         ────────────────────── (!R)        ──────────────────────────────── (!R)                            ──────────────────────────────── (!R)        ────────────────────────────────────────── (!R)                                                                                                                                      
                                                                                                    B, A, Q |- F, !D                          Q |- B, A, F, !D                                                                                 C, Q |- D, E, A, !B                    C, Q |- D, E, !A, !!B                                            C, Q |- !D, !E, A, !B                            C, Q |- !D, !E, !A, !!B                                                                                                                                                     
                                                                       ──────────────── (I)        ──────────────────────── (!R)             ──────────────────────── (!L)        ────────────────── (I)                                      ─────────────────────────── (vR)   ───────────────────────────────────── (vR)                       ───────────────────────────────────── (vR)   ─────────────────────────────────────────────── (vR)                                                                     ─────────────── (F)                                         
                                                                       A, Q |- A, F, !D               A, Q |- !B, F, !D                         !B, Q |- A, F, !D                 !B, Q |- !B, F, !D                                            C, Q |- (A v !B), D, E                 C, Q |- (!A v !!B), D, E                                         C, Q |- (A v !B), !D, !E                         C, Q |- (!A v !!B), !D, !E                                                                                     E, D, C, Q |- F                                             
                                                                       ──────────────────── (!L)   ───────────────────────────── (!L)        ───────────────────────────── (!L)   ────────────────────── (!L)                                 ───────────────────────────────────────────────────────────────────────────── (^R)                  ───────────────────────────────────────────────────────────────────────────────────────────────── (^R)                             ────────────────── (I)             ─────────────────── (!R)                                    
                                                                        !A, A, Q |- F, !D               !!B, A, Q |- F, !D                        !A, !B, Q |- F, !D               !!B, !B, Q |- F, !D                                                            C, Q |- ((A v !B) ^ (!A v !!B)), D, E                                                                        C, Q |- ((A v !B) ^ (!A v !!B)), !D, !E                                                               D, C, Q |- F, D, E                  D, C, Q |- F, !E                                           
                                                                       ────────────────────────────────────────────────────────────── (vL)   ──────────────────────────────────────────────────────────────── (vL)                            ────────────────────────────────────────────────────────────────────────────────── (!L)             ────────────────────────────────────────────────────────────────────────────────────────────────────── (!L)                        ────────────────────── (!R)        ──────────────────────── (!R)                               
                                                                                         A, Q, (!A v !!B) |- F, !D                                              !B, Q, (!A v !!B) |- F, !D                                                                          !((A v !B) ^ (!A v !!B)), C, Q |- D, E                                                                       !((A v !B) ^ (!A v !!B)), C, Q |- !D, !E                                                             C, Q |- F, !D, D, E                  C, Q |- F, !D, !E                                        
                                                                       ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── (vL)                       ─────────────────────────────────────────────────────────────────────────────────────── (!R)        ─────────────────────────────────────────────────────────────────────────────────────────────────────────── (!R)                   ─────────────────────────── (vR)   ───────────────────────────── (vR)                          
                                                                                                                            Q, (A v !B), (!A v !!B) |- F, !D                                                                                                          C, Q |- !!((A v !B) ^ (!A v !!B)), D, E                                                                      C, Q |- !!((A v !B) ^ (!A v !!B)), !D, !E                                                           C, Q |- (D v E), F, !D             C, Q |- (!D v !E), F, !D                                  
                                                                       ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── (^L)                  ──────────────────────────────────────────────────────────────────────────────────────────── (vR)   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────── (vR)              ───────────────────────────────────────────────────────────────────── (^R)                     
                                                                                                                             ((A v !B) ^ (!A v !!B)), Q |- F, !D                                                                                                       C, Q |- (D v E), !!((A v !B) ^ (!A v !!B))                                                                   C, Q |- (!D v !E), !!((A v !B) ^ (!A v !!B))                                                                     C, Q |- ((D v E) ^ (!D v !E)), F, !D                                           
    ─────────────────────────────────────────────────────── (I)        ───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── (!R)             ───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── (^R)         ────────────────────────────────────────────────────────────────────────── (=>R)               
    !((A v !B) ^ (!A v !!B)), Q |- !((A v !B) ^ (!A v !!B))                                                                    Q |- !((A v !B) ^ (!A v !!B)), F, !D                                                                                                                                                           C, Q |- ((D v E) ^ (!D v !E)), !!((A v !B) ^ (!A v !!B))                                                                                                                Q |- (C => ((D v E) ^ (!D v !E))), F, !D                                      
    ─────────────────────────────────────────────────────────── (!R)   ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── (vR)        ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── (=>R)   ──────────────────────────────────────────────────────────────────────────────── (vR)          
     Q |- !!((A v !B) ^ (!A v !!B)), !((A v !B) ^ (!A v !!B))                                                                   Q |- (F v !D), !((A v !B) ^ (!A v !!B))                                                                                                                                                        Q |- !!((A v !B) ^ (!A v !!B)), (C => ((D v E) ^ (!D v !E)))                                                                                                            Q |- (F v !D), (C => ((D v E) ^ (!D v !E)))                                  
    ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── (^R)   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── (^R)     
                                                                                  Q |- !((A v !B) ^ (!A v !!B)), (!!((A v !B) ^ (!A v !!B)) ^ (F v !D))                                                                                                                                                                                                                Q |- (C => ((D v E) ^ (!D v !E))), (!!((A v !B) ^ (!A v !!B)) ^ (F v !D))                                                                                                                                    
    ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── (^R)
                                                                                                                                                                                                                                      Q |- (!((A v !B) ^ (!A v !!B)) ^ (C => ((D v E) ^ (!D v !E)))), (!!((A v !B) ^ (!A v !!B)) ^ (F v !D))                                                                                                                                                                                                                                        
    ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── (vR)
                                                                                                                                                                                                                                       Q |- ((!((A v !B) ^ (!A v !!B)) ^ (C => ((D v E) ^ (!D v !E)))) v (!!((A v !B) ^ (!A v !!B)) ^ (F v !D)))

Operator Precedence & Associativity

In order of precedence:

Operator	Opeartor (symbolic)	Associativity
not	!	N/A (prefix operator)
and	^	Associative
xor	+	Associative
or	v	Associative
implies	=>	Right-Associative
iff	<=>	Associative
if-then-else	( ? : )	N/A (must always be enclosed in parantheses)

For instance

subexpressions (A ? (B ? C : D) : E xor not F and G implies H or I iff J)

would be interpreted as

subexpressions (A ? (B ? C : D) : (((E xor (not F and G)) implies (H or I)) iff J))

Saving Outputs

As mentioned previously, boolexman pipes its output through less to provide a more convenient interface to its users, which in turn, also allows them to save the output of the commands they execute.

To save the output of a command:

Execute your command as usual.
Press s (small-case!) while viewing the output of your command.
- You should see a prompt at the bottom of your terminal log file: , if not, check the documentation of your operating system (your version of less might not have this functionality).
- To cancel, press BACKSPACE; the prompt at the bottom of your terminal should turn back into : or (END).
Enter the name of the file you would like to save into, and press ENTER (RETURN).
- If the file(name) you just entered already exists, you'll see the warning Warning: "FILENAME" exists; Overwrite, Append or Don't log? at the prompt of less. Pressing O will overwrite, and pressing D will cancel the operation. You can also press A to append to the file, but that is probably not what you want.
Done! The prompt at the bottom of your terminal should turn back into : or (END).

Command Syntax

In its most general form:

<VERB> <VERB SPECIFIC ARGUMENTS...>

The definitions below should be decipherable to many, although beware that none of them are formal definitions (especially with respect to the spaces).

<VERB>
```
[A-Za-z]+
```
<SYMBOL>
```
[A-Z][a-z]*
```
True and False are reserved symbols, meaning true and false respectively.
<LIST OF SYMBOLS>
```
\[<SYMBOL>(, <SYMBOL>)*\]
```
<PREFIX OPERATOR>
```
(!  |  not)
```

<INFIX OPERATOR>

(and  |  ^  |  xor  |  \+  |  or  |  v  |  implies  |  =>  |  iff  |  <=>)

<ITE EXPRESSION>

\((if <EXPRESSION> then <EXPRESSION> else <EXPRESSION>  |  <EXPRESSION> \? <EXPRESSION> : <EXPRESSION>)\)

<EXPRESSION>

(<SYMBOL>  |  <PREFIX OPERATOR> <EXPRESSION>  |  <EXPRESSION> <INFIX OPERATOR> <EXPRESSION>  |  <ITE EXPRESSION>)

License

The ISC License, see LICENSE for details.

Notice

Beware that boolexman used to use GNU Readline library prior to the commit c93cb4350823832fc42883661f152c523d767bd4, but mistakenly said to be licensed under The ISC License where it should have been The General Public License (due to the Copyleft clause).

Acknowledgements

In no specific order, I am grateful

to Prof. Michael Fourman for teaching us the principles of logic, which I relied on extensively in developing this program, and of computation.
to Prof. Don Sannella for teaching us functional programming, which enabled me to complete this program in less than two months thanks to the expressivity (and type system) of Haskell.
and to both of them, because Curry–Howard correspondence! =)

Name		Name	Last commit message	Last commit date
Latest commit History 42 Commits
src		src
web		web
.gitignore		.gitignore
ChangeLog.md		ChangeLog.md
LICENSE		LICENSE
README.md		README.md
Setup.hs		Setup.hs
boolexman.cabal		boolexman.cabal

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

src

src

web

web

.gitignore

.gitignore

ChangeLog.md

ChangeLog.md

LICENSE

LICENSE

README.md

README.md

Setup.hs

Setup.hs

boolexman.cabal

boolexman.cabal

Repository files navigation

boolexman

Setup

Running the Tests

Compiling the Web Application from the Sources

Quick Manual

Command Verbs

Operator Precedence & Associativity

Saving Outputs

Command Syntax

License

Notice

Acknowledgements

About

Releases 2

Packages

Languages

License

boramalper/boolexman

Folders and files

Latest commit

History

Repository files navigation

boolexman

Setup

Running the Tests

Compiling the Web Application from the Sources

Quick Manual

Command Verbs

Operator Precedence & Associativity

Saving Outputs

Command Syntax

License

Notice

Acknowledgements

About

Topics

Resources

License

Stars

Watchers

Forks

Languages