TALK KEYWORD INDEX

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

A | |

ACTL | |

Algorithm portfolios | |

Amortized Analysis | |

Answer set programming | |

antichain-based tree automata language inclusion | |

API | |

Arithmetic Circuits | |

Automata | |

automata learning | |

Automated reasoning | |

Axiomatisation | |

B | |

belief revision | |

bit-width | |

Boolean Operations | |

bounded model checking | |

C | |

Cardinality Constraints | |

CEGAR | |

Clause Learning | |

Cognitive Reasoning | |

Complexity | |

Computational Complexity | |

Computer algebra | |

Constrained Uniform Sampling | |

constraint satisfaction | |

Constraint Solving | |

Convex optimization | |

Coq | |

Cost Semantics | |

counterexample | |

Counterfactual Reasoning | |

Craig Interpolation | |

cyclic graphs | |

Cyclic proofs | |

D | |

d-DNNF | |

data mining | |

Data streaming | |

deadlock | |

Decidability | |

decision procedures | |

Default Logic | |

Deontic Logic | |

Description Logic | |

Description Logics | |

Digital library | |

Distributed IC3 | |

Distributed SMT | |

Divide-and-conquer | |

Domain agnostic | |

E | |

ECTL | |

efficient reasoning | |

epistemic logic | |

EPR | |

Equational Reasoning | |

Erlang | |

Ethical Decision Making | |

event lists | |

exclusive-or | |

experimental evaluation | |

F | |

finite model finder | |

finite satisfiability | |

First-order logic | |

Fluent Calculus | |

Formal languages and automata theory | |

Formal verification | |

Fragments of first-order logic | |

Function Summaries | |

Functor | |

G | |

Game theory | |

Games | |

Garbage Collection | |

general satisfiability | |

Geometry of Interaction | |

gossip protocols | |

graph games | |

graph rewriting | |

Groupoid | |

Gödel logics | |

H | |

Halpern-Shoham Logic | |

Herbrand expansions | |

Hierarchical systems | |

Higher Inductive Type | |

Homotopy Type Theory | |

I | |

implementations | |

Incremental Verification | |

Induction | |

inductive definitions | |

Infeasibility analysis | |

Infinite alphabets | |

infinite descent | |

infinite trees | |

inprocessing techniques | |

Integer linear programming | |

interference | |

Interior Point Method | |

Interpolation | |

Interval Logic | |

Invariant generation | |

Isabelle/HOL | |

K | |

Kleene algebra | |

Knowledge Compilation | |

knowledge-based protocols | |

Kripke Semantics | |

L | |

Lambda Calculus | |

Lamport clocks | |

Lattice Basis Reduction | |

lazy learning | |

linear inequalities | |

LL(1) parsing | |

logic and computational complexity | |

Logic Programming | |

Lookahead Heuristic | |

Loop | |

LP Solving | |

LTL with arithmetic | |

Lyndon interpolation | |

M | |

Matching | |

metaqueries | |

Minimal unsatisfiable subsets | |

Modal Logic | |

model checking | |

Model Predictive Control | |

Modelling | |

Monotonicity | |

multigraphs | |

MUS enumeration | |

mutable memory | |

N | |

Nash equilibrium | |

Nonmonotonic Proof Calculus | |

Numerical Software Verification | |

Nuprl | |

O | |

Omega-regular languages | |

Operational Semantics | |

P | |

parity games | |

path orderings | |

Pattern matching | |

Polymorphism | |

Program analysis | |

Program verification | |

progress measure | |

Proof checker | |

Propositional Satisfiability | |

protocol verification | |

pushdown automata | |

Q | |

quantified bit-vectors | |

R | |

Random walks and Markov chains | |

rational synthesis | |

Reachability games | |

read-over-write simplification | |

regular languages | |

relational database | |

resource analysis | |

Resource Bound Analysis | |

Reversible Computations | |

rewrite orderings | |

S | |

SAT | |

SAT solving | |

satisfiability modulo theories | |

Satisfiability Modulo Theory | |

Skolemization | |

SMT encoding | |

SMT Solving | |

Software Verification | |

Stable models | |

Static Analysis | |

Sub-propositional Fragments | |

Success Types | |

Succinctness | |

symbolic computation | |

symmetry breaking | |

T | |

Tableaux System | |

termination | |

The guarded fragment | |

The two-variable fragment | |

theory of arrays | |

Three-Valued Lukasiewicz Logic | |

Tree Automata | |

two-variable logic with counting quantifiers | |

Type Inference | |

Type Systems | |

Types | |

U | |

Univalence | |

unranked trees/forests | |

Unsatisfiability analysis | |

V | |

verification | |

Verified theorem prover backend | |

W | |

Weak Completion | |

web-based GUI | |

witness | |

word combinatorics | |

Y | |

YubiHSM | |

YubiKey |