Algorithms on Atomic Representations of Herbrand Models

摘要

The importnace of models within automated deduction is generally acknowledged both in constructing countermodels (rather than just giving the answer "NO", if a given formula is found to be not a theorem) and in speeding up the deductio nprocess itself (e.g. by semantic resolution refinement).