Sciweavers

Share
LOPSTR
1998
Springer

Using Decision Procedures to Accelerate Domain-Specific Deductive Synthesis Systems

9 years 8 months ago
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.
Jeffrey Van Baalen, Steve Roach
Added 06 Aug 2010
Updated 06 Aug 2010
Type Conference
Year 1998
Where LOPSTR
Authors Jeffrey Van Baalen, Steve Roach
Comments (0)
books