Mixing Finite Success and Finite Failure in an Automated Prover
Alwen Tiu, Gopalan Nadathur, Dale Armin Miller · 2005
Abstract. The operational semantics and typing of modern programming and specification languages are often defined using relations and proof systems. In simple settings, logic programming can be used to provide rather direct and natural interpreters for such operational semantics. More complex features of specifications such as names and their bindings, proof rules with negative premise, and the exhaustive enumeration of state spaces, all pose significant challenges to conventional logic programming systems. In this paper, we describe a simple architecture for the implementation of deduction systems that allows a specification to interleave both with finite success and finite failure. The implementation techniques for this prover are largely common ones from logic programming, i.e., logic variables, (higher-order pattern) unification, backtracking (using stream-based computation), and abstract syntax based on simply typed λ-terms. We present a particular instance of this prover architecture and its prototype implementation, based on a dual interpretation of (finite) success and failure in proof search. We discuss important differences between this prover and traditional logic programming and present an implementation of bisimulation checking for π-calculus, which cannot be so directly and declaratively done in traditional logic programming languages. 1