TALK KEYWORD INDEX

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

A | |

Abduction | |

absoluteness | |

Algebra | |

Algebraic Data Types | |

Algebraic Datatypes | |

algebras | |

approximation algorithm | |

associative-commutative | |

ATP | |

automated reasoning | |

automated theorem proving | |

Automation | |

B | |

Beth Definability | |

binary decision diagrams | |

bit-vectors | |

Bitvectors | |

Büchi games / parity games | |

C | |

CHC Transformations | |

clausal proof | |

Clause Elimination | |

clause ordering | |

Clause Selection | |

coinduction | |

Combination method | |

Combinatorics | |

Combinators | |

Combinatory logic | |

Commutativity | |

Competition | |

compilation | |

Complete theories | |

Completeness | |

concrete domains | |

concurrent dynamic logic | |

Conditional rewriting | |

Congruence closure | |

connection tableau calculus | |

Constrained Horn Clauses | |

constraint satisfaction | |

constructibility | |

Constructive Logic | |

Convex Polyhedra | |

Convex theories | |

Coq | |

Coq Proof Assistant | |

countable transitive models | |

Covers | |

cryptography | |

cyclic proofs | |

D | |

decidability | |

Decidability and complexity | |

Decision problem | |

Decision Procedure | |

decision procedures | |

Decision Trees | |

demodulation | |

dependent type theory | |

dependent types | |

Description logic | |

domain-specific languages | |

Dominance | |

Dyadic logic | |

E | |

E prover | |

elliptic curve | |

ELPI | |

embeddings | |

ENIGMA | |

Equational reasoning | |

extensibility | |

Extensionality | |

F | |

Feasibility | |

Feasible Interpolation | |

finite boundedness | |

Finite satisfiability | |

first-order logic | |

first-order theorem proving | |

Fixed-point arithmetic | |

fixpoint logic | |

focusing | |

forcing | |

formal proofs | |

formal verification | |

Formalisation of Mathematics | |

Formalization of Mathematics | |

formalized mathematics | |

functional analysis | |

Functors | |

G | |

Game Logic | |

GCIs | |

generated theorem prover | |

generic extension | |

Geometry Algorithm | |

Groebner basis | |

Ground identities | |

group law | |

H | |

Higher-order | |

Higher-Order Logic | |

HOL | |

homogeneity | |

Hybrid Games | |

Hybrid Logic | |

hygiene | |

hyperresolution | |

Hypersequent calculi | |

I | |

induction | |

Inductive Datatypes | |

inference guidance | |

Infinity axioms | |

inhabitation | |

Integer arithmetic | |

interactive theorem proving | |

interpolation | |

Introsort | |

intuitionistic logic | |

intuitionistic modal logic | |

iprover | |

Isabelle | |

Isabelle-LLVM | |

Isabelle/HOL | |

Isabelle/ZF | |

isomorph-free exhaustive generation | |

L | |

Lambek's restriction | |

Layered selection | |

lean | |

lemma names | |

linear logic | |

literal selection | |

Liveness Analysis | |

LLVM | |

Logic | |

logic programming | |

logical framework | |

M | |

Machine Learning | |

macros | |

mathematical components | |

mathematical notation | |

mathematical structures | |

MCSAT | |

mechanised mathematics | |

meta model | |

meta-parameters | |

Meta-properties | |

metaprogramming | |

Mizar | |

MMT | |

modal logic | |

model checking | |

Model computation | |

model revision | |

model theory | |

Monadic decomposition | |

Monadic first-order logic | |

monotone modal logic | |

monotone mu-calculus | |

multi-conclusion systems | |

Multi-way Join | |

multiplexing rule | |

N | |

nested sequents | |

Neural Networks | |

non-commutative logic | |

Non-normal modal logics | |

nonmonotonic logic | |

normal form | |

normalization | |

O | |

omega-admissibility | |

ontology | |

ordered resolution | |

Ordered Structures | |

orderly generation | |

P | |

Pdqsort | |

pedagogical example | |

Polite theories | |

Polymorphism | |

Presburger arithmetic | |

Program analysis | |

programmer's text editor | |

Prolog | |

Proof Assistant | |

proof assistants | |

proof automation | |

proof engineering | |

proof search | |

Proof System | |

proof tactic | |

proof theory | |

Provers | |

Q | |

QBF Proof System | |

QRAT | |

Quantified Boolean Formulas | |

Quantifier Expansion | |

Quicksort | |

Quotient Types | |

R | |

Rank-1 | |

Real arithmetic | |

Reduction classes | |

Redundancy | |

Regular Expressions | |

reinforcement learning | |

resolution | |

Results | |

Runtime Verification | |

S | |

SAT | |

SAT solving | |

Satisfiability | |

satisfiability checking | |

satisfiability games | |

Satisfiability modulo theories | |

saturation | |

saturation theorem proving | |

Saturation-based theorem proving | |

Saturation-Style Proving | |

Sequent calculus | |

SGGS | |

simplification | |

SMT | |

software verification | |

Soundness | |

SSA form | |

Strategy Extraction | |

stratified fragment | |

streams | |

Strings | |

subexponentials | |

substructural logic | |

Suggested Upper Merged Ontology | |

SUMO | |

superposition | |

superposition calculus | |

symmetry breaking | |

Syntax-Guided Synthesis | |

Synthetic un/decidability in Coq | |

System Competition | |

T | |

Temporal Logic | |

Term ordering | |

term rewriting | |

Termination | |

termination tool | |

theorem prover | |

Theorem proving | |

Theories | |

Theory Combination | |

Theory Reasoning | |

tool | |

Trakhtenbrot theorem | |

transitive closure | |

U | |

ultrafilters | |

ultraproducts | |

undecidability | |

unification hints | |

Uniform quantifier-free interpolation | |

universal algebra | |

V | |

Vampire | |

Variable independence | |

verification | |

Verified Compilation | |

Verified Efficient Algorithms | |

W | |

Web-based application | |

Word problem | |

X | |

XGBoost |