works on
clause selection 1first-order logic 1goal-directedness 1saturation-based proving 1term sharing 1

From the 1 of 1 linked paper with an AI index.

collaborators

1 paper

cs.LO2026

Some Experiments with Twee-Style Goal-Directedness

Stephan Schulz

The paper extends the Twee approach of preferring clauses that share terms with the conjecture to full first-order saturation-based theorem proving, proposing a shared-term impleme…