IPC solver
Description
It determines whether a given statement in Intuitionistic Propositional Calculus (IPC) is provable or not.
Dependencies
- OCaml
- MiniSat executable (for refutation by Kripke models)
- LaTeX (for drawing proof diagrams)
Usage (Command Line)
$ make
$ ./ipc_solver <<< "~~(A \/ ~A)"
$ ./ipc_solver <<< "A \/ ~A"
Usage (LaTeX)
$ make
$ ./ipc_solver --latex ipc.tex <<< "~~(A \/ ~A)"
$ latex ipc.tex
$ dvipdfmx ipc.dvi
Usage (Twitter Bot)
Please prepare your consumer key, consumer secret, access token, and access token secret.
$ make
$ cp twitter-config.rb.example twitter-config.rb
$ vim twitter-config.rb
$ bundle exec ruby twitter.rb