First-Order Logic in Finite Domains: Where Semantic Evaluation Competes with SMT Solving

Wolfgang Schreiner, Franz-Xaver Reichl

In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first…