TALK KEYWORD INDEX

This page contains an index consisting of author-provided keywords.

A | |

alpha-equivalence | |

assumption-based reasoning | |

ATP | |

automated reasoning | |

automated theorem proving | |

Automatic program verification | |

Automatic theorem proving | |

B | |

benchmarks | |

C | |

CDCL | |

clausal tableaux | |

combinators | |

condensed detachment | |

connection structure calculus | |

Connection tableaux | |

Constraint Horn clauses | |

COST | |

D | |

decision procedure | |

Dedukti | |

E | |

EuroProofNet | |

F | |

first-order ATP | |

first-order logic | |

First-order logic with equality | |

first-order reasoning | |

First-order theorem proving | |

G | |

grammar-based tree compression | |

Graph Neural Networks | |

H | |

heuristics | |

Horn theories | |

I | |

induction | |

Isabelle | |

L | |

Lazy paramodulation | |

learning | |

logic languages | |

M | |

model building | |

N | |

Non-classical Logic | |

non-classical logics | |

non-redundant clause learning | |

P | |

performance prediction | |

preprocessing | |

proof compression | |

proof schemas | |

Proof search | |

proof structures | |

Proofs | |

Python | |

Q | |

QBF | |

R | |

run-time performance | |

S | |

SAT | |

Saturation | |

SCL | |

SGGS | |

shallow embedding | |

Skolem | |

SMT | |

strategy scheduling | |

superposition | |

T | |

term orderings | |

theorem proving | |

TPTP | |

TPTP World | |

Tseitin | |

two-watched literal scheme | |

U | |

user benchmark |