proplog

A solver for propositional logic, with a HTTP server, all written in Prolog.
git clone git://seanh.sh/proplog
Log | Files | Refs | README | LICENSE

README.md (4820B)


      1 # proplog
      2 
      3 An educational resource for those just starting propositional logic.
      4 
      5 Pipe a file of line-separated predicates to the `unix_cmd.pl` script simply to test it out,
      6 or run `./server.pl` to get an API/frontend running on localhost:3000.  It responds differently depending
      7 on the Content-Type header in http request.
      8 
      9 Here's an example usage of the test via stdin workflow:
     10 
     11 ```
     12 # cat homework.txt
     13 ((a v b) ^  ~b) -> (a v b ^ c)
     14 # cat homework | ./unix_cmd.pl
     15 ┌─┬─┬─┬─────────┬────┬────────────────┬───────┬─────────────┬───────────────────────────────┐
     16 │a│b│c│'(a v b)'│'~b'│'((a v b) ^ ~b)'│'b ^ c'│'(a v b ^ c)'│'((a v b) ^ ~b) -> (a v b ^ c)'│
     17 ├─┼─┼─┼─────────┼────┼────────────────┼───────┼─────────────┼───────────────────────────────┤
     18 │0│0│0│        0│   1│               0│      0│            0│                              1│
     19 ├─┼─┼─┼─────────┼────┼────────────────┼───────┼─────────────┼───────────────────────────────┤
     20 │0│0│1│        0│   1│               0│      0│            0│                              1│
     21 ├─┼─┼─┼─────────┼────┼────────────────┼───────┼─────────────┼───────────────────────────────┤
     22 │0│1│0│        1│   0│               0│      0│            0│                              1│
     23 ├─┼─┼─┼─────────┼────┼────────────────┼───────┼─────────────┼───────────────────────────────┤
     24 │0│1│1│        1│   0│               0│      1│            1│                              1│
     25 ├─┼─┼─┼─────────┼────┼────────────────┼───────┼─────────────┼───────────────────────────────┤
     26 │1│0│0│        1│   1│               1│      0│            1│                              1│
     27 ├─┼─┼─┼─────────┼────┼────────────────┼───────┼─────────────┼───────────────────────────────┤
     28 │1│0│1│        1│   1│               1│      0│            1│                              1│
     29 ├─┼─┼─┼─────────┼────┼────────────────┼───────┼─────────────┼───────────────────────────────┤
     30 │1│1│0│        1│   0│               0│      0│            1│                              1│
     31 ├─┼─┼─┼─────────┼────┼────────────────┼───────┼─────────────┼───────────────────────────────┤
     32 │1│1│1│        1│   0│               0│      1│            1│                              1│
     33 └─┴─┴─┴─────────┴────┴────────────────┴───────┴─────────────┴───────────────────────────────┘
     34 #
     35 ```
     36 # Examples
     37 
     38 http://localhost:3000/tableau?q=%28a+v+%7Ea%29+%5E+%28b+v+%7Eb%29+%5E+%28c+v+%7Ec%29
     39 
     40 ## TODO
     41 As a result of the satisfiability problem, this script will eat your server if you let people pass input with excessive variables in.  E.g. 32 variable expression = a 2 ** 32 row table
     42 
     43 ## TODO
     44 Update the README.md to reflect changes made to server.
     45 
     46 ## TODO
     47 Redefine 'success' for tableau as *either* finding a contradiction *or* finding a full derivation tree (i.e. no contradiction, and therefore ~S is invalid).