A naive model generator, model checker and theorem prover
for some combinations of classical and intuitionistic, non-modal and modal, propositional and first-order logic, analytic tableau and sequent calculus.
This software can compute
- the denotation (truth value) of a given logical expression in a given structure,
- a tableau or sequent deduction tree with associated minimal (counter) models for a given inference or set of sentences.
© Natalie Clarius [email protected]
License: CC BY-NC-SA 4.0 (https://creativecommons.org/licenses/by-nc-sa/4.0/).
You can try the model checking feature out here.
If you want to dive in deeper, I recommend downloading pyPL to your own computer.
To run this software locally on your machine:
- Install dependencies:
- Download this repository.
- Execute
pyPL/main.py.
Documentation on how to enter formulas, structures and input files can be found in pyPL/doc/parser.md.
Some sample input files are available in pyPL/input.
Generated output files are stored in pyPL/output.
Information on the functionality of some of the buttons and options are shown as tooltips on mouse hover.
For troubleshooting information, see pyPL/doc/troubleshooting.md.
If that doesn't help, please open a GitHub issue or e-mail me.
Some background on the theory underlying the implementation can be found in pyPL/doc/paper.pdf.
- theorem proving: generate an analytic tableau or sequent tree to show that a formula or inference is valid/invalid
- (counter) model generation: generate a minimal structure in which a given (set of) formulas is true/false
- model checking: evaluation of expressions relative to structures, variable assignments and possible worlds
- truth table generation
- propositional logic
- first-order logic with zero-place predicates, function symbols and term equality
- intensional logic with operators □, ◇, ^, ⱽ; propositional, constant and varying domains; frame K
- intuitionistic logic with Kripke semantics (only model checking)
- three-valued logic (not yet implemented)
- analytic tableaux
- sequent calculus (classical logic only)
- input of formulas and structures with ordinary keyboard characters, directly or from a file
- output in plain text or LaTeX-generated PDF
- model checking works only on structures with finite domains
- model generation and theorem proving works only on formulas of relatively small size due to performance limitations
- tableau algorithm relatively inefficient
- GUI and parser can be glitchy (window not scrollable, buttons sometimes not behaving as expected, parser not always recognizing bracketing correctly)
- global variables are bad
- useful feedback on incorrectly entered input rather than no parser response
- more efficient proof search and model generation
- in model checking, print out detailed derivation rather than just final result of evaluation
- broader coverage:
- lambda calculus and e-t type theory
- more frames for modal logic; temporal logic; model generation and modal logic for intuitionistic logic
- tableaus with free variables
- other frameworks and calculi, e.g. DRT, ND
- This implementation is an experimental proof-of-concept. It is not efficient or designed for real-life applications.
- Although the software has been extensively tested, I do not guarantee soundness. Use at your own risk.
© 2021-2024 Natalie Clarius <[email protected]> nclarius.github.io
This work is licensed under the GNU General Public License v3.0.
This program comes with absolutely no warranty.
This is free software, and you are welcome to redistribute and/or modify it under certain conditions.
I am glad to receive comments, bug reports and improvement suggestions via GitHub issues or e-mail to [email protected].
