Completeness for inductive procedures

We propose a new approach to delineating logics of programs, based directly on inductive definition of program semantics. The ingredients are elementary and well-known, but their fusion yields a simple yet powerful approach, surprisingly overlooked for ...

We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an ...

Automated inductive reasoning for term rewriting has been extensively studied in the literature. Classes of equations and term rewriting systems (TRSs) with decidable inductive validity have been identified and used to automatize the inductive ...