Implementing a fair monodic temporal logic prover
Michel Ludwig, Ullrich Hustadt · AI Communications · 2010
Monodic first-order temporal logic is a fragment of first-order temporal logic for which sound and complete calculi have been devised. One such calculus is ordered fine-grained resolution with selection, which is implemented in the theorem prover TeM