@deontic-logic/proof-tool

Contents

1. Introduction
2. License
3. Dependencies
4. Building
   1. Building on Linux
   2. Building on Windows

Introduction

GUI application based on wxWidgets to explore formulas, structures and proofs.

• Syntax and semantics based on Nortmann's DL³ system. A modal extension of classical propositional logic and the alethic logic S5.
• Symbolic representation of DL-formulas similar to their visual representation in LaTeX, internally using Scalable Vector Graphic (SVG) rendering.
• Abstract syntax tree generation of DL-formulas using an Earley parser with a custom Context-free grammar.
  • Calculate pretty layouts for abstract syntax trees via the Reingold–Tilford algorithm, and compose them into SVGs.
  • View generated 'geometry only' SVGs, which are rendered using code of the library igagis/svgren and its dependencies (all MIT-licensed).
    
• Condensed detachment proof parser based on tree unification, taking the most efficient approach of formula substitution by direct modifications of shared nodes.
  • Ability to parse pmproofs.txt of the mmsolitaire project – concerned with finding minimal proofs – into a proof collection.
    Most efficient parser known so far. Also includes a multi-threaded generator for minimal proofs that is eligible for shared memory high-performance computing, and can be used to generate improved versions of pmproofs.txt. This feature can be found isolated and without custom axiom support at xamidi/pmGenerator with a command-line interface.
    Exemplary generated results are available at xamidi/mmsolitaire. If you have access to a powerful computer, please consider to use this feature to further contribute to our knowledge regarding minimal proofs.
• DL-structures:
  • Decide definition properties
    
  • DL-formula evaluation and obligation verification
    
  • View, edit, count
    
  • Generate lists of representatives and random samples
• DL-proofs:
  • Integrated editor for proofs based on conditional syntactic consequence
    
    
    
    
    
    
  • Validity checks, including conditional validation with custom axioms
  • Proof unfolding and reduction
  • LaTeX code generation
  • A Metamath executable output interpreter to load proofs
  • Metamath parser and converter for .mm files

License

Each file is released as stated in a file named LICENSE that is contained in the closest directory which also contains said file. That is, direct contributions to this repository are released under the GNU Lesser General Public License v3.0, but whenever third-party code is made part of the project, the original license of the author applies. In all such cases the original license requires to be at least as permissible as LGPLv3, so that for binaries of proof-tool, all the LGPLv3 permissions, restrictions and conditions apply. For example, while all files in nortmann/ adapt the LGPLv3 license from their parent directory, all files in svgren/ are kept under their original MIT license.

Dependencies

• Boost.Algorithm (header-only ; verified: v1.80.0 ; license: Boost Software License v1.0)
• Boost.Iostreams (see above)
• Boost.Multiprecision (see above)
  • GNU Multiple Precision Arithmetic Library (verified: v6.1.2 ; license: LGPLv3)
    or Multiple Precision Integers and Rationals (verified: v2.7.2 ; license: LGPLv3)
• Boost.Random (see above)
• Cairo (verified: v1.15.12, v1.16.0, v1.17.2 ; license: Mozilla Public License v1.1)
• oneTBB 2021.5+ (verified: v2021.5.0, v2021.6.0 ; license: Apache License 2.0)
• wxWidgets 3.1 (verified: v3.1.2, v3.1.3 ; license: wxWindows Library Licence v3.1 ; deficient: v3.1.4 – 3.2.1 [Why?])

When using GCC for compilation, another dependency is the GNU C++ Library, licensed under GCC Runtime Library Exception v3.1.

Note that all dependencies have licenses permissible enough to make static linking an option when publishing under LGPLv3.

Building

Since the Boost libraries are header-only, there are 4 dependencies which require binaries:

1. Cairo
2. GMP or MPIR
3. oneTBB
4. wxWidgets

Builds of proof-tool succeeded on Linux using GCC from managed packages (which must support at least C++20), and on Windows using standalone builds of MinGW-w64-based GCC and Clang/LLVM, such as available on winlibs.com.

The building process is straghtforward. For example, internal builders of IDEs such as Eclipse CDT can be used on both platforms, or you may generate makefiles with an appropriate tool such as GNU Automake.

Building on Linux

Dependencies can be built or installed on Linux distributions by following the corresponding software project's instructions, and then be used with the settings below. For further information such as potentially useful compiler or linker configurations, follow the instructions for Windows.

Include Paths

-I${PROJECT_HOME}/svgren -I/usr/local/lib/wx/include/gtk3-unicode-3.1 -I/usr/local/include/wx-3.1

Library Search Paths

-L/usr/local/lib

Library Includes

-pthread -ltbb -lgmp -lcairo -lwx_baseu-3.1 -lwx_gtk3u_core-3.1 -lwx_gtk3u_stc-3.1

Building on Windows

Detailed exemplary building instructions and results can be found at releases/results_v2.

It should be noted that the GNU linker ld is very slow on Windows. When using GCC as a compiler, it is beneficial to use the LLVM linker lld by adding

-fuse-ld=lld

to the linker flags. MSYS2 is a reliable source of frequently updated dynamic link libraries for development on Windows.