ausblenden:
Schlagwörter:
-
Zusammenfassung:
Two apparently different approaches to automating deduction are mentioned in
the title; they are the subject of a debate on ``big engines vs.\ little
engines of proof''. The contributions in this thesis advocate that these two
strands of research can interplay in subtle and sometimes unexpected ways, such
that mutual pervasion can lead to intriguing results: Firstly, superposition
can be run on top of decision procedures. This we demonstrate for the class of
Shostak theories, incorporating a little engine into a big one. As another
instance of decision procedures within superposition, we show that ground
confluent rewrite systems, which decide entailment problems in equational
logic, can be harnessed for detecting redundancies in superposition
derivations. Secondly, superposition can be employed as proof-theoretic means
underneath combined decision procedures: We re-establish the correctness of the
Nelson-Oppen procedure as an instance of the completeness of superposition.
Thirdly, superposition can be used as a decision procedure for many interesting
theories, turning a big engine into a little one. For the theory of bits and of
fixed-size bitvectors, we suggest a rephrased axiomatization combined with a
transformation of conjectures, based on which superposition decides the
universal fragment. Furthermore, with a modification of lifting, we adapt
superposition to the theory of bounded domains and give a decision procedure,
which captures the Bernays-Schönfinkel class as well.
