GLOBAL TALK KEYWORD INDEX

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

A | |

abstraction | |

accessibility | |

ACL2s | |

Array-based transitions systems | |

Asymptotically-tight | |

ATP | |

ATP System | |

Attestation logics | |

Automated Deduction | |

Automated Deduction in Geometry | |

Automated First-Order Theorem Proving | |

automated geometry proving | |

Automated grading | |

Automated Induction | |

automated reasoning | |

automated theorem proving | |

Automatic Complexity Analysis | |

Automatic feedback | |

automatic theorem provers | |

automatic theorem proving | |

automatic-theorem-prover | |

avatar | |

Award | |

Awards | |

Axiomatic Theories of Truth | |

B | |

bana-comon | |

Basic Paramodulation | |

Best Papers | |

Bill McCune | |

binary decision diagram | |

Bounded Model Checking | |

Break 1 | |

Break 2 | |

Break 3 | |

C | |

C Programs | |

CADE | |

Case Analysis | |

ccsa | |

CDCL | |

CDSAT | |

certificate | |

Chromium | |

clause selection | |

Closed Forms | |

Cloud | |

CNF | |

collatz conjecture | |

Combination | |

commonsense reasoning | |

Competition | |

completeness | |

complexity | |

Complexity Analysis | |

Compliance | |

computational complexity | |

computational model | |

computer-assisted mathematics | |

Condensed Detachment | |

Connection Method | |

Constraint | |

contexts | |

Coq | |

COQ plugin | |

countable | |

Counter-example generation | |

D | |

Darkside | |

Datalog | |

Decidability of Termination | |

decision procedure | |

deductive verification | |

deep inference | |

defeasible deontic logic | |

delta-complete decision procedures | |

dependent type | |

dependent type theory | |

derivational complexity | |

Description Logic | |

Description Logics | |

deVrijer’s proof | |

diagrams | |

discovery | |

Disjunctive | |

domain-specific language | |

DSL | |

dynamic geometry software | |

Dynamic Geometry Systems | |

E | |

Edinburgh Logical Framework | |

Education | |

EL | |

Elektron | |

elimination | |

entailment problems | |

Equational Reasoning | |

Equational Theorem Proving | |

estimating probability | |

Euclidean planar geometry | |

evaluation | |

Exercise Generation | |

Expected Runtimes | |

Expected Sizes | |

Explanations | |

explicit | |

external prover | |

F | |

Facilitating | |

Fast | |

first-class Booleans | |

first-order logic | |

first-order resolution | |

first-order theorem proving | |

Formal Mathematics | |

formal methods | |

formal proof | |

Formal proofs | |

formal verification | |

formalization | |

Functional Programming | |

G | |

GATP | |

Generation | |

GeoGebra | |

geometric inequality | |

geometry | |

Geometry automated theorem provers | |

GPU | |

graph | |

graph convolutional network | |

Guidance | |

H | |

Hacking | |

Halting Problem | |

hard typing | |

Herbrand | |

Heuristics | |

higher-order logic | |

Higher-order Pattern Unification | |

higher-order rewriting | |

Hyper tableau | |

I | |

IDE | |

IMO Grand Challenge | |

Implementation | |

Implicational Logic | |

induction | |

inductive definitions | |

Inductive Reasoning | |

inductive type | |

Inference | |

inprocessing clausification | |

integer induction | |

integer programming | |

Integrity constraints | |

Interactive Proof Assistant | |

interactive theorem proving | |

Internet routing | |

Interpretation Methods | |

interpreted Boolean type | |

intuitionistic logic | |

Intuitionistic Propositional Logic | |

isabelle | |

Isabelle Proof Assistant | |

Isabelle/VSCode | |

ITP | |

J | |

JavaRes | |

K | |

Knuth-Bendix completion | |

L | |

labelled tableaux | |

Lace | |

lambda-calculus | |

Law | |

Learned | |

Learning | |

Lemmas | |

Linear constraint loops | |

LLVM | |

Local Tracing | |

Logic | |

Logic programming | |

logical framework | |

Logical Frameworks | |

logical relation | |

logical transformation | |

logical transformations | |

Logics | |

Loop | |

M | |

machine learning | |

many-one reduction | |

Mathematica | |

Mathematical Induction | |

mathematical software | |

mathematics education | |

mathematics for engineers | |

matrix interpretations | |

Mechanizing Meta-Theory | |

Meeting | |

Meta Level Reasoning | |

meta logic | |

meta-logic | |

Meta-Theory | |

MetaCoq | |

metalogic | |

Modal Logics | |

Model computation | |

Model construction | |

models | |

modularity | |

Morality | |

Multiphase-linear ranking functions | |

Multivariate | |

N | |

Natural Language Processing | |

Nelson-Openn | |

Networked | |

Newbie | |

next step guidance | |

Nipkow | |

Node.js | |

Non-classical | |

non-Fregean logics | |

non-linear constraint solving | |

non-linear real arithemic | |

Non-Termination | |

Normal Forms | |

normative reasoning | |

O | |

object logic | |

olympiad | |

Opening | |

Optimizations | |

Order-Sorted Algebras | |

P | |

Parallel | |

parallelism | |

Parametric Systems | |

Place | |

Policy based routing | |

Polite Combination | |

Polynomial bounds | |

Polynomial Loops | |

polynomial termination | |

polynomials | |

Positive Almost Sure Termination | |

Probabilistic | |

Probabilistic Integer Programs | |

Project | |

projective geometry | |

Proof | |

proof assistant | |

Proof assistants | |

Proof automation | |

proof certificates | |

proof checking | |

proof explanation | |

proof logging | |

Proof procedures | |

proof reconstruction | |

Proof Representations | |

Proof search | |

proof strategy | |

proof tactic | |

proof terms | |

Proofs | |

Property based testing | |

Propositional Logic | |

Prover | |

pseudo-Boolean | |

PyRes | |

Q | |

QEPCAD B | |

quantified Boolean formula | |

R | |

real quantifier elimination | |

Reasoning | |

Reception | |

Recursion | |

recursive neural networks | |

Redundancy | |

Reflection | |

refutational completeness | |

reinforcement learning agents | |

relevance | |

Religion | |

Repair | |

resolution | |

resolution method | |

Results | |

rewriting | |

ruler and compass constructions | |

runtime complexity | |

S | |

SAT | |

satisfiability | |

Satisfiability Modulo Theories | |

satisfiability solving | |

saturation | |

saturation-based theorem proving | |

Secondary schools geometry proofs | |

security protocols | |

Sentential Calculus with Identity | |

Separation Logic | |

Sequent calculus | |

Serverless | |

services | |

set of support | |

Shared Memory | |

Simplification | |

simplification ordering | |

Simply typed lambda calculus | |

Skolem | |

SML | |

SMT | |

SMT solvers | |

SMT solving | |

soft typing | |

Solving | |

SOS | |

splitting | |

static analysis | |

string rewriting | |

Strong normalization | |

Structural Induction | |

subformula linking | |

SUMO | |

superposition | |

Sylvan | |

symbol precedence | |

Symbolic Execution | |

Symbolic integration | |

system description | |

T | |

Tactics | |

Tarski | |

TBA | |

TBA1 | |

TBA2 | |

TBA3 | |

Techniques | |

term rewriting | |

Term Rewriting Systems | |

termination | |

Termination analysis | |

The 2020 | |

The 2021 | |

Theorem | |

theorem prover | |

theorem proving | |

Theory Combination | |

Theory of Computation | |

Tobias | |

Topical | |

TPTP | |

TPTP problem set | |

TPTP World | |

Tracing | |

transcendental functions | |

translation | |

Trust | |

Truth Predicate | |

Turing machines | |

type systems | |

type theory | |

Typescript | |

U | |

uncertain reasoning | |

Uncertainty Principle | |

undecidability | |

Unification | |

unit equality | |

unsatisfiability proofs | |

user interface | |

User interfaces | |

V | |

Vampire | |

W | |

Ways | |

Woody Bledsoe | |

Work-stealing | |

Worst-case | |

Z | |

Zipperposition |