ipc_solver:OCaml中的O(N log N)个空间IPC解算器 源码

IPC求解器 描述 它确定直觉命题演算(IPC)中的给定语句是否可证明。 依存关系 OCaml MiniSat可执行文件(供Kripke模型驳斥) LaTeX(用于图纸验证图) 用法(命令行) $ make $ ./ipc_solver <<< "~~(A \/ ~A)" $ ./ipc_solver <<< "A \/ ~A" 用法(LaTeX) $ make $ ./ipc_solver --latex ipc.tex <<< "~~(A \/ ~A)" $ latex ipc.tex $ dvipdfmx ipc.dvi 用法