TALK KEYWORD INDEX

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

A | |

analyticity | |

Answer Set Programming | |

Approximations | |

ATL+ | |

Automata | |

automated deduction | |

automated theorem prover | |

B | |

background theories | |

backward proof search | |

Bayesian networks | |

binary decision diagrams | |

bounded model checking | |

C | |

circumscription | |

coalgebra | |

codatatypes | |

Combination problem | |

Comparative evaluations | |

completeness of first-order logic | |

complex networks | |

complexity | |

complexity analysis | |

conditional logics | |

Congruence Closure | |

connection calculus | |

constrained clauses | |

constrained ordered resolution | |

Context-based Reasoning | |

cut elimination | |

cut-introduction | |

cyber-physical systems | |

D | |

data structures for tableaux calculi | |

decidability | |

decision method | |

decision procedures | |

Description Logics | |

Differential Temporal Dynamic Logic | |

dynamic logic | |

E | |

Equality | |

equational logic | |

equational simplification | |

F | |

first order logic | |

first-order logic | |

first-order modal logic | |

Fixpoints | |

Floating-point arithmetic | |

focused derivations | |

Forgetting | |

Formal verification | |

Fractal Dimension | |

G | |

geometry | |

global assumptions | |

global caching | |

H | |

Haskell | |

higher-order logic | |

Hilbert Axioms | |

hybrid systems | |

Hypersequent Calculi | |

I | |

Implementation and Optimisation Techniques | |

intuitionistic | |

intuitionistic propositional logic | |

inverse roles | |

J | |

Java | |

L | |

lazy data structures | |

local theories | |

local theory extensions | |

logic | |

Logic solvers | |

lower bounds | |

M | |

Minimal model generation | |

modal logic | |

Modal logics | |

Modal Logics of Confluence | |

modal tableaux | |

model checking | |

Model construction | |

model generation | |

Model-checking | |

model-finding | |

N | |

nested sequent calculi | |

nominals | |

non-classical logics | |

non-deterministic semantics | |

Non-disjoint union of theories | |

non-monotonic logics | |

Number Restrictions | |

O | |

Ontologies | |

ontology | |

Ontology Reasoning | |

optimization | |

Otter | |

OWL 2 EL | |

P | |

Permutation lemmas | |

pointer arithmetic | |

preprocessing | |

primal infon logic | |

prime implicates | |

program analysis | |

Prolog | |

proof checking | |

proof complexity | |

proof compression | |

proof search | |

proof theory | |

propositional logics | |

Propositional Normal Modal logics | |

Propositional Resolution | |

Q | |

QBF | |

R | |

reduction to SAT | |

resolution | |

Resolution Method | |

Rewriting | |

S | |

SAT | |

SAT Features | |

SAT solver | |

satisfiability | |

Satisfiability Modulo Theories | |

Satisfiability procedure | |

saturation | |

Saturation Procedures | |

Scala | |

Self-similarity | |

sequent calculi | |

sequent calculus | |

SHOIQ | |

SHQ | |

simulations | |

SMT | |

SMT-solving | |

Software Verification | |

Solver competitions | |

Solver execution services | |

string processing | |

strong termination | |

subset-simulation | |

System description | |

T | |

Tableau | |

Tableau Algorithms | |

tableaux | |

tableaux calculus | |

Tarski | |

temporal logic | |

temporal logics | |

term rewriting | |

termination | |

theorem proving | |

Theorem-Proving | |

tool support | |

U | |

Uncertainty Reasoning | |

Uniform Interpolation | |

V | |

verification | |

Visibly Pushdown Languages |