88 citations · 94 across the 4 of their papers we have counts for
4 papers
Some Experiments with Twee-Style Goal-Directedness
Stephan Schulz
In saturation-based theorem proving, selecting the next clause for processing is a major concern. Twee has successfully applied the idea of preferring clauses that share terms with…
MizAR 60 for Mizar 50
Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel +6
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60\% of the Mizar theorems in the hammer setting. We also automatically pr…
ProofWatch: Watchlist Guidance for Large Theories in E
Zarathustra Goertzel, Jan Jakubův, Stephan Schulz +1
Watchlist (also hint list) is a mechanism that allows related proofs to guide a proof search for a new conjecture. This mechanism has been used with the Otter and Prover9 theorem p…
New results on rewrite-based satisfiability procedures
Alessandro Armando, Maria Paola Bonacina, Silvio Ranise +1
Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literal…