TALK KEYWORD INDEX
This page contains an index consisting of author-provided keywords.
A | |
AI | |
ALCH | |
auction theory | |
automate reasoning | |
automated reasoning | |
automated theorem proving | |
Autonomous systems | |
B | |
Boolean Algebra and Presburger Arithmetic | |
C | |
CDCL algorithm | |
classical logic | |
Constraints | |
CSP | |
D | |
definability | |
deontic logic | |
E | |
economics | |
Expressive Description Logics | |
Extended resolution | |
F | |
first-order logic | |
Focus Groups | |
Forgetting | |
Forgetting/projection/uniform interpolation | |
formal methods | |
Formal verification | |
functional programming | |
G | |
General resolution | |
H | |
Herbrand theorem | |
Heuristics | |
higher-order | |
Human Reasoning | |
hybrid automata | |
I | |
Interactive Theorem Provers | |
intuitionistic logic | |
M | |
mechanism design | |
Minimal model generation | |
modal logic | |
model generation | |
modular verification | |
multi agent | |
N | |
natural deduction | |
normal modal logics | |
P | |
parallel deduction | |
parameter synthesis | |
planning | |
program equivalence | |
program verification | |
proof complexity | |
proof search | |
Propositional proof system | |
Q | |
query rewriting | |
R | |
Reconfiguration | |
regression verification | |
resolution | |
Resolution Method | |
Robots | |
S | |
SAT solving | |
Satisfiability Modulo Theories | |
search | |
Second-order quantifier elimination | |
sequent calculus | |
socratic proofs | |
SPA | |
Strongest Necessary Conditions | |
subset-simulation | |
superposition | |
T | |
Tableau | |
Tableaux calculi | |
temporal logic | |
term indexing | |
term ordering | |
Theorem-Proving | |
U | |
Uniform Interpolation | |
Usability | |
V | |
verification |