@@ -199,9 +199,9 @@ Basic DISCOUNT loop from @braniac:
199199Knuth Bendix Order:
200200- efficient version based on @kbo
201201- efficiently extended to literals like duper
202- - function symbol precende like in @braniac :
202+ - precedence between function symbols like in @braniac :
203203 - higher arity wins
204- - same arity use arbitrary order from term bank
204+ - same arity: arbitrary order, here: index within term bank
205205
206206Unification:
207207- the naive algorithm from the lecture
@@ -235,7 +235,7 @@ For tautology checking:
235235
236236== Subsumption
237237Heuristic based on @subsume :
238- - order literals to work likely harder ones earlier
238+ - order literals by likelihood to work: harder ones earlier
239239- afterwards bruteforce using an efficient backtracking
240240 scheme like in @zipperposition
241241- uses a feature vector index for forward/backward substitution
@@ -248,11 +248,9 @@ Ran TPTP Problems on privately owned hardware:
248248- Memory Limit of 1GB
249249- 16 Instances in parallel
250250
251- CASC runs the problems sequentially on one CPU socket with a lot higher memory limit,
252- but it is not feasible for us while testing with private hardware.
253-
254- // TODO: cite or delete
255- Initially used the pelletier problems, which are easy but are very broad.
251+ CASC:
252+ - sequential runs on one CPU socket with a lot higher memory limit
253+ - infeasible for us while testing with private hardware
256254
257255== CASC
258256# grid (
0 commit comments