Logics Workbench 1.0
Logics Workbench 1.0
复制标题
逻辑工作台1.0
DOI：
--
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
Stefan Schwendimann
中科院分区：
文献类型：
--
作者：
P. Balsiger;Alain Heuerding;Stefan Schwendimann
证明者：逻辑工作台 (LWB)，版本 1.0。请参阅 LWB 主页了解更多信息。 LWB 在两侧序贯演算中进行向后证明搜索。对于 S4，我们使用循环检查来确保终止。通过“use-check”，我们切断了由具有两个前提的可逆规则生成的不必要的分支；如果例如在证明 Δ ⊃ A, Γ 时，公式 A 没有被‘使用’，那么我们知道 Δ ⊃ A ∧ B, Γ 也是可证明的。重复的公式将被删除。结构共享有助于减少公式和序列的复制。没有启发法。编程语言：C++。编译器：Sun C++ 4.0.1。操作系统：Solaris 2.4。可用性：LWB 1.0 的二进制文件可通过 LWB 主页获取（选择 LWB，安装 LWB）。您还可以通过 WWW 使用 LWB 1.0。在 LWB 主页上选择通过 WWW 运行会话并输入您的请求。证明器的附加设施：图形用户界面、内置编程语言、进度指示器（滑块显示证明搜索的进行情况）、证明搜索的踪迹可用、转换公式的各种功能。硬件：Sun SPARCstation 5，主存：80MB，1 个CPU（70 MHz microSPARC II） 时序：时序包括公式的解析和相应数据结构的构建。 LWB加载的文件具有以下形式：load(s4);时间开始；可证明（框 p0 -> 框框 p0）；时间停止；辞职;
Prover: Logics Workbench (LWB), version 1.0. See the LWB home page for more information. The LWB does backward proof search in two-sided sequent calculi. In the case of S4 we use a loop-check in order to ensure termination. With ‘use-check’ we cut off unnecessary branches generated by invertible rules with two premises; if e.g. in the proof of ∆ ⊃ A, Γ the formula A is not ‘used’, then we know that ∆ ⊃ A ∧ B, Γ is provable as well. Duplicate formulas are deleted. Structure sharing helps to reduce the copying of formulas and sequents. No heuristics. Programming language: C++ . Compiler: Sun C++ 4.0.1 . Operating system: Solaris 2.4 . Availability: The binaries of the LWB 1.0 are available via the LWB home page (choose about the LWB, install the LWB). You can also use the LWB 1.0 via WWW. Choose run a session via WWW on the LWB home page and type in your request. Additional facilities of the prover: Graphical user interface, built-in programming language, progress indicator (a slider shows how the proof search is going on), trace of the proof search is available, various functions to convert formulas. Hardware: Sun SPARCstation 5, main memory: 80MB, 1 CPU (70 MHz microSPARC II) Timing: The timing includes parsing of the formulas and the construction of the corresponding data structure. The files loaded by the LWB have the following form: load(s4); timestart; provable(box p0 -> box box p0); timestop; quit;