The astronomical domain involves shallow proofs with many axioms. Set-of-support focuses on goals rather than axioms.

Problem: combination of restrictions loses completeness.

• Set-of-support

• Recursive path ordering

• Constructiveness

Contents    Page-10    Prev    Next    Page+10    Index