TALK KEYWORD INDEX

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

A | |

abduction | |

abstraction refinement | |

Actions | |

anti-unification | |

arithmetic constraints | |

artificial intelligence | |

Associativity | |

automated reasoning | |

automated theorem proving | |

B | |

Bayesian Machine Learning | |

benchmarking | |

Bernays–Schönfinkel Fragment | |

binary codes | |

C | |

Calculus of Names | |

Choice logics | |

clause learning from simple models | |

clause redundancy | |

closure redundancy | |

Cloud Security | |

Commonsense reasoning | |

Commutativity | |

complexity | |

complexity analysis | |

concurrency | |

connectedness | |

consequence relations | |

Constraint tableaux | |

counter systems | |

countermodel construction | |

CTL* | |

Cut Elimination | |

cut-elimination | |

Cyclic proofs | |

Cylindrical Algebraic Coverings | |

D | |

Data analysis | |

decidability | |

Decidable Subclasses | |

Default logic | |

definitions | |

Description Logic | |

Description Logic EL | |

Diagonalizable matrices | |

differential dynamic logic | |

E | |

Effective algorithms | |

entailment | |

equational unification | |

evaluation | |

Eventual non-negativity | |

explanation | |

F | |

factor interpretation | |

finite axiomatizability | |

first-order logic | |

First-order logic with equality | |

First-order theorem proving | |

Formula Simplification | |

Fuzzy proximity relations | |

G | |

Generalization | |

Geometry Problem Solving | |

ground joinability | |

Gödel logic | |

H | |

Haskell | |

Higher-order logic | |

Hilbert-style proof systems | |

Hypersequents | |

I | |

infeasibility | |

integer programs | |

integer transition systems | |

Invariance | |

Isabelle/HOL | |

J | |

justifications | |

L | |

Lambek calculus | |

Le\'sniewski | |

Linear Arithmetic | |

Linear dynamical systems | |

linear logic | |

Linear recurrence sequences | |

loop acceleration | |

lower runtime bounds | |

M | |

machine learning | |

maximum satisfiability | |

MaxSAT | |

Minimal tableau | |

minimal unsastisfiable set | |

minimality criterion | |

modal logic | |

Modal logics | |

N | |

NMatrices | |

nominal logic | |

Non-deterministic Semantics | |

non-monotonic reasoning | |

non-termination | |

nonlinear real arithmetic | |

O | |

ontology | |

P | |

Paraconsistency | |

parametric solution | |

path orders | |

Pigeonhole principle | |

Planning | |

preferences | |

preprocessing | |

preserving primitivity | |

prime implicates | |

Procedure | |

proof-search | |

Proof-search heuristics | |

Proofs | |

propagation redundancy | |

propagation redundant proof | |

Propositional Dynamic Logic | |

propositional intermediate logics | |

propositional logic | |

Q | |

Quantitative theories | |

R | |

randomization | |

reachability | |

Redundancy Elimination | |

Refutation calculus | |

Relevance | |

rewriting logic | |

S | |

SAT solving | |

Satisfiability | |

Satisfiability Modulo Theories | |

saturation-based theorem proving | |

Separation Logic | |

Sequent Calculi | |

Sequent Calculus | |

SMT | |

sound and complete calculus | |

strategy scheduling | |

Subexponentials | |

substitution | |

Subsumption | |

superposition | |

symbolic reachability | |

syntax with bindings | |

Synthetic tableau | |

T | |

Tableaux | |

term rewriting | |

Termination | |

theorem proving | |

Theory of Sequences | |

TPTP | |

Transitive Closure Logic | |

Two-dimensional logics | |

type theory | |

U | |

upper runtime bounds | |

V | |

Verification | |

verification of hybrid systems | |

Visualization |