Propositional and First Order Logic Tool to analyse formula

145 Views Asked by At

I am looking for an online tool which analyses a given propositional and/or first order logic formula.

For example the tool should output, whether the given formula is satisfiable, its rank, ...

If you know any other good online tools, I'm happy too (computing interpolant, kripke models, herbrand expansion, hilbert system, ...)

1

There are 1 best solutions below

0
On

"I am looking for an online tool which analyses a given ... first order logic formula. For example the tool should output, whether the given formula is satisfiable."

That would decide whether a closed formula is a first-order theorem.

Wouldn't that be nice!

Impossible though.

As was proved back in the 1930s, there is no "tool" (no procedure that can be implemented on a computer, at any rate) that can decide theoremhood for arbitrary first-order sentences.

https://en.wikipedia.org/wiki/Entscheidungsproblem