Skip to content

qnighy/ipc_solver

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

65 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

About

O(N log N)-space IPC solver in OCaml

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages