Using Decision Procedures to Build Domain-Specific Deductive Synthesis Systems
Jeffrey VanBaalen, S. Roach, Sonie Lau · 1998
This paper describes a class of decision procedures that we have found useful for efficient, domains-pecific deductive synthesis. These procedures are called closure-based ground literal satisfiability procedures. We argue that this is a large and interesting class of procedures and show how to interface these procedures to a theorem prover for efficient deductive synthesis. Finally, we describe some results we have observed from our implementation. Amphion/NAIF...