4
$\begingroup$

I have

  • a formula $\varphi$ of propositional modal logic or propositional intuitionistic logic,

  • a finite Kripke frame $W$,

and I would like to test whether $\varphi$ is valid in $W$.

This is an enumeration of finitely many possibilities (and in the cases I am interested in the “finite” isn't even so large, so it's probably doable by hand, but it would be tedious), so I'd rather like to have a computer do this for me.

Is there a preexisting piece of software¹ that would help me do this? (Either directly solving the problem or transforming it to a form that can be passed to a boolean SAT-solver.) I can write it myself, but the probability of making an error would be much higher than if the software already exists…

  1. Open source and able to run under Linux; and I guess I should also add “not completely bitrotten in 2025” as a constraint because, sadly, reasearch software which worked in 2000 might fail to compile in 2025.
Improve this question
$\endgroup$
3
  • 2
    $\begingroup$ You could ask at proofassistants.stackexchange.com with a better chance of an answer. $\endgroup$ Commented Apr 8 at 18:32
  • $\begingroup$ Dumb question: can this not easily be encoded into SAT? $\endgroup$ Commented Apr 15 at 14:36
  • 2
    $\begingroup$ @cody Indeed, although it may depend on your definition of “easily” — mathematically there is on difficulty, but actually writing the code is tedious. Anyway, this is what I ended up doing (writing some Perl code to call a SAT-solver). I'll probably post a self-reply once I get around to seriously testing the code and writing a README file. $\endgroup$ Commented Apr 15 at 16:46

1 Answer 1

Reset to default
6
$\begingroup$

So I ended up writing my own program for the intuitionistic case. It can be found here on GitHub. As an example, I used it to generate this document tabulating the validity of a number of sample formulas on a number of sample frames:

First page of a document showing a table of validities of various intuitionistic formulas over various Kripke frames. At the top is a table giving the satisfaction of the formulas over the frames, and below is a table of the formulas themselves.

Second page of a document showing a table of validities of various intuitionistic formulas over various Kripke frames. This page shows the last two formulas, and then frames graphically as oriented graphs.

(The frames named skvortsov-1 through skvortsov-10 are taken from the paper “Сравнение дедуктивной силы реализуемых пропозициональных формул” [=“Comparison of the deductive power of realizable propositional formulas”] by Dmitry Pavlovich Skvortsov [=Дмитрий Павлович Скворцов], Логические исследования [=Logical Investigations] 3 (1995) 38–52, drawings on pages 51–52; several formula in my list are also taken from that paper.)

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ I am both terrified and amazed that you wrote it in Perl. $\endgroup$ Commented Apr 17 at 13:49
  • $\begingroup$ @AndrejBauer For all its flaws, Perl is very very good at one thing, and that's manipulating character strings (like, parsing stuff and talking to other programs). $\endgroup$ Commented Apr 17 at 13:52
  • 1
    $\begingroup$ I had my share of Perl, I know. I am now tempted to implement the same thing in Lean so that it's proved correct. $\endgroup$ Commented Apr 17 at 13:57
  • $\begingroup$ @AndrejBauer Now I am the one who is both terrified and amazed! $\endgroup$ Commented Apr 17 at 13:58

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.