A DCEC* prover written in Java powered by SNARK first-order theorem prover.

The current fork can be found here on our GitHub.

Algorithm Sketch:

Every atomic modal formula m is assigned a unique propositional variable s: We call s the propositional shadow of m. For any formula f[ m,..], the corresponding formula f[ s,..], with all atomic modal formulae replaced by their propositional shadows, is called the shadow of f[ m,..].

• Step 1: The prover first replaces all occurrences of atomic modal formulae by propositional variables (even nested occurrences). Now we have a first-order problem.
• Step 2: Call a first-order prover (SNARK) on this first-order problem.
• Step 3: If the first-order prover fails, we expand the premises with any legal modal rule (via forward reasoning natural deduction) and repeat the process from Step 1. If the prover succeeds, we return true.