1996/08/01 by Suresh Subramanian · 3 citations
Computer Science · Mathematics · #Formal Methods in Verification #Logic, programming, and type systems #Algorithms and Data Compression #Checkerboard #Parameterized complexity #Automated theorem proving #Computer science #Gas meter prover #Theoretical computer science #Mathematical proof #Algorithm #Lisp #Discrete mathematics #Mathematics #Calculus (dental) #Programming language #Geometry
paper · doi:10.1093/logcom/6.4.573
openalex publication_date 1996/08/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
We present a method of modelling parameterized classes of finite state machines in the Boyer-Moore logic so that invariant properties can be verified interactively using the Boyer-Moore theorem prover. We illustrate our approach using an interactive proof of the impossibility of covering an n × n ‘mutilated’ checkerboard completely with dominoes. We model the problem by defining a simulator and formalize the well-known parity argument as a proof by mathematical induction on the length of action sequences executed starting with an empty board. The suitability of our approach for verifying properties depends strongly on the actual Lisp data structures and programs used in the simulation model. We explain some of the choices we made in simplifying the checkerboard problem representation and describe in detail the heuristic guidance given to the theorem prover.