Using Decision Procedures to Accelerate Domain-Specific Deductive Synthesis Systems

This paper describes a class of decision procedures that we have found useful for efficient, domain-specific deductive synthesis, and a method for integrating this type of procedure into a general-purpose refutation-based theorem prover. We suggest that this is a large and interesting class of procedures and show how to integrate these procedures to accelerate a general-purpose theorem prover doing deductive synthesis. While much existing research on decision procedures has been either in isolation or in the context of interfacing procedures to non-refutation-based theorem provers, this appears to be the first reported work on decision procedures in the context of refutationbased deductive synthesis where witnesses must be found.

• Type: Conference
• Year: 1998
• Where: LOPSTR
• Authors: Jeffrey Van Baalen, Steve Roach
• Keywords: Automated Reasoning, Decision Procedures, Deductive Synthesis, LOPSTR 1998, Procedures