TALK KEYWORD INDEX

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

A | |

A* proof search | |

Abduction | |

ALC | |

algebra | |

Antichains | |

Antipatterns | |

automata theory | |

automated complexity analysis | |

automated reasoning | |

automated theorem prover | |

Automated Theorem Proving | |

axiomatization | |

B | |

Basic Feasible Functionals | |

BBI | |

blocked clauses | |

Boolean Pythagorean Triples problem | |

bunched calculi | |

C | |

Chains | |

clause elimination | |

complexity | |

computational complexity | |

computational complexity of reasoning | |

Confluent Rewrite Relations | |

connection method | |

Constrained Horn clauses | |

constraint satisfaction | |

Context-free languages | |

Continuation passing style | |

Coq | |

Crowdsourcing | |

cut-elimination | |

D | |

deep inference | |

Deep Learning | |

description logic | |

Diagrammatic Reasoning | |

Dilworth's theorem | |

distributive substructural logics | |

domain specific language | |

DRAT proofs | |

Dunn-Mints calculi | |

E | |

educational logic software | |

epistemic logic | |

evaluation strategies | |

F | |

fair termination | |

First Order Theory | |

First-Order Logic | |

formal proofs | |

G | |

gossip protocols | |

Graph reachability | |

Graph Rewriting | |

Gödel logic | |

H | |

Hall's theorem | |

Higher order complexity | |

higher-order logic | |

Higher-Order Modal Logic | |

horn clause solving | |

Horn solving | |

hypersequents | |

I | |

implication problem | |

inclusion dependency | |

independence | |

independence atom | |

Inductive invariant | |

infinite lists | |

interactive theorem proving | |

interpolation | |

Interpretations | |

Isabelle/HOL | |

K | |

knowledge based programs | |

Knowledge Representation | |

L | |

linear arithmetic | |

linear logic | |

linear nested sequents | |

Linear Temporal Logic | |

Linearization | |

logic of bunched implications | |

logical frameworks | |

LTL | |

LTL to automata translation | |

M | |

machine learning | |

Maximum independent set | |

MELL | |

Memory Management Unit | |

memory models | |

Mirsky's theorems | |

Model Checking | |

model expansion | |

modular systems | |

monadic fragment | |

multimodalities | |

N | |

nondeterminism | |

O | |

omega-automata | |

Ontologies | |

Operating Systems | |

Overlapping Rewrite Systems | |

P | |

Parallel Rewriting | |

paramodulation | |

Partial Model Checking | |

Partially ordered sets | |

Past Operators | |

preprocessing | |

probabilistic programs | |

Program analysis | |

Program Verification | |

Proof Assistant | |

proof automation | |

proof search | |

proof theory | |

propagators | |

Propositional satisfiability | |

Q | |

Quantitative Reasoning | |

query optimization | |

R | |

reasoner | |

relational logic | |

Relational verification | |

resolution calculus | |

resource types | |

S | |

sat | |

SAT solving | |

Semantical Embedding | |

semi-deterministic automata | |

Semiring | |

separation logic | |

serious games | |

software model checking | |

solvers | |

Soundness | |

Stateflow | |

structural rules | |

superposition | |

symbolic transducer | |

system description | |

T | |

tableau proofs | |

Tableaux | |

term rewriting | |

Theorem Proving | |

Tractable classes | |

Translation Lookaside Buffer | |

Type Theory | |

U | |

Unbounded model checking | |

uniformity |