A Decomposition Rule for Decision Procedures by Resolution-Based Calculi.
Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. basic superposition, a calculus highly optimized for theorem proving with equality. However, even such an advanced calculu...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Journal article |
| Language: | English |
| Published: |
Springer
2004
|