TALK KEYWORD INDEX

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

A | |

Array-based transitions systems | |

ATP | |

ATP System | |

Attestation logics | |

Automated First-Order Theorem Proving | |

automated reasoning | |

automated theorem proving | |

automatic theorem provers | |

avatar | |

Award | |

Awards | |

B | |

Basic Paramodulation | |

Best Papers | |

Bill McCune | |

binary decision diagram | |

Break 1 | |

Break 2 | |

Break 3 | |

C | |

CDCL | |

clause selection | |

collatz conjecture | |

Combination | |

commonsense reasoning | |

Competition | |

completeness | |

complexity | |

Compliance | |

computational complexity | |

computer-assisted mathematics | |

Condensed Detachment | |

Connection Method | |

D | |

Darkside | |

decision procedure | |

deep inference | |

defeasible deontic logic | |

delta-complete decision procedures | |

dependent type theory | |

Description Logic | |

Description Logics | |

diagrams | |

domain-specific language | |

DSL | |

E | |

EL | |

entailment problems | |

Equational Reasoning | |

Equational Theorem Proving | |

estimating probability | |

Explanations | |

F | |

Fast | |

first-class Booleans | |

first-order resolution | |

first-order theorem proving | |

Formal Mathematics | |

formal verification | |

Functional Programming | |

G | |

geometry | |

graph convolutional network | |

H | |

Herbrand | |

Heuristics | |

higher-order logic | |

Hyper tableau | |

I | |

IMO Grand Challenge | |

Implementation | |

Implicational Logic | |

induction | |

inductive definitions | |

inprocessing clausification | |

integer induction | |

Interactive Proof Assistant | |

interactive theorem proving | |

Interpretation Methods | |

interpreted Boolean type | |

intuitionistic logic | |

Intuitionistic Propositional Logic | |

isabelle | |

ITP | |

K | |

Knuth-Bendix completion | |

L | |

labelled tableaux | |

Law | |

Learning | |

Lemmas | |

Logic programming | |

Logical Frameworks | |

Logics | |

M | |

machine learning | |

many-one reduction | |

matrix interpretations | |

Mechanizing Meta-Theory | |

Meeting | |

metalogic | |

Modal Logics | |

Model computation | |

Model construction | |

models | |

Morality | |

N | |

Natural Language Processing | |

Nelson-Openn | |

Newbie | |

Nipkow | |

Non-classical | |

non-Fregean logics | |

non-linear constraint solving | |

Normal Forms | |

normative reasoning | |

O | |

olympiad | |

Opening | |

Optimizations | |

Order-Sorted Algebras | |

P | |

Parametric Systems | |

Place | |

Polite Combination | |

polynomials | |

Proof assistants | |

Proof automation | |

proof checking | |

proof explanation | |

Proof procedures | |

proof reconstruction | |

Proof Representations | |

Proof search | |

proof terms | |

Proofs | |

Prover | |

Q | |

quantified Boolean formula | |

R | |

Reception | |

recursive neural networks | |

Redundancy | |

refutational completeness | |

reinforcement learning agents | |

Religion | |

Repair | |

resolution method | |

Results | |

S | |

SAT | |

Satisfiability Modulo Theories | |

satisfiability solving | |

saturation | |

saturation-based theorem proving | |

Sentential Calculus with Identity | |

Separation Logic | |

Sequent calculus | |

set of support | |

Simplification | |

simplification ordering | |

Skolem | |

SMT | |

SMT solvers | |

SMT solving | |

SOS | |

splitting | |

string rewriting | |

subformula linking | |

superposition | |

symbol precedence | |

Symbolic integration | |

system description | |

T | |

TBA | |

Techniques | |

term rewriting | |

termination | |

The 2020 | |

The 2021 | |

Theorem | |

theorem prover | |

theorem proving | |

Theory Combination | |

Tobias | |

Topical | |

transcendental functions | |

Trust | |

U | |

uncertain reasoning | |

Unification | |

unit equality | |

user interface | |

W | |

Ways | |

Woody Bledsoe | |

Z | |

Zipperposition |