A |

A* proof search | TacticToe: Learning to Reason with HOL4 Tactics |

ALC | RACCOON: A Connection Reasoner for the Description Logic ALC |

algebra | Propagators and Solvers for the Algebra of Modular Systems |

automated complexity analysis | Analyzing Runtime Complexity via Innermost Runtime Complexity |

automated reasoning | Blocked Clauses in First-Order Logic TacticToe: Learning to Reason with HOL4 Tactics RACCOON: A Connection Reasoner for the Description Logic ALC |

automated theorem proving | Theorem Provers For Every Normal Modal Logic Blocked Clauses in First-Order Logic |

axiomatization | On the Interaction of Inclusion Dependencies with Independence Atoms |

B |

basic feasible functionals | Higher order interpretation for higher order complexity |

BBI | Bunched Hypersequent Calculi for Distributive Substructural Logics |

blocked clauses | Blocked Clauses in First-Order Logic Towards a Semantics of Unsatisfiability Proofs with Inprocessing |

Boolean Pythagorean Triples problem | Formally Proving the Boolean Pythagorean Triples Conjecture |

bunched calculi | Bunched Hypersequent Calculi for Distributive Substructural Logics |

C |

clause elimination | Blocked Clauses in First-Order Logic |

complexity | On the Interaction of Inclusion Dependencies with Independence Atoms |

computational complexity | Quantified Boolean Formulas: Call the Plumber! |

Confluent Rewrite Relations | Parallel Graph Rewriting with Overlapping Rules |

connection method | RACCOON: A Connection Reasoner for the Description Logic ALC |

Constrained Horn Clauses | Synchronizing Constrained Horn Clauses |

constraint satisfaction | Decidable linear list constraints |

context-free languages | Cauliflower: a Solver Generator for Context-Free Language Reachability |

continuation-passing style | Automated analysis of Stateflow models |

Coq | Coq without Type Casts: A Complete Proof of Coq Modulo Theory |

cut elimination | Bunched Hypersequent Calculi for Distributive Substructural Logics |

D |

deep inference | Deep Proof Search in MELL |

deep learning | Deep Network Guided Proof Search |

Description Logic | RACCOON: A Connection Reasoner for the Description Logic ALC |

distributive substructural logics | Bunched Hypersequent Calculi for Distributive Substructural Logics |

DRAT proofs | Towards a Semantics of Unsatisfiability Proofs with Inprocessing |

Dunn-Mints calculi | Bunched Hypersequent Calculi for Distributive Substructural Logics |

E |

educational logic software | Quantified Boolean Formulas: Call the Plumber! |

evaluation strategies | Analyzing Runtime Complexity via Innermost Runtime Complexity |

F |

first-order logic | Blocked Clauses in First-Order Logic Deep Network Guided Proof Search |

first-order theory | Coq without Type Casts: A Complete Proof of Coq Modulo Theory |

formal proofs | Formally Proving the Boolean Pythagorean Triples Conjecture |

G |

graph reachability | Cauliflower: a Solver Generator for Context-Free Language Reachability |

graph rewriting | Parallel Graph Rewriting with Overlapping Rules |

Gödel logic | Gödel logics and the fully boxed fragment of LTL |

H |

Higher-order complexity | Higher order interpretation for higher order complexity |

higher-order logic | Theorem Provers For Every Normal Modal Logic TacticToe: Learning to Reason with HOL4 Tactics |

Higher-Order Modal Logic | Theorem Provers For Every Normal Modal Logic |

Horn Clause Solving | Quantified Heap Invariants for Object-Oriented Programs |

hypersequents | Bunched Hypersequent Calculi for Distributive Substructural Logics |

I |

implication problem | On the Interaction of Inclusion Dependencies with Independence Atoms |

inclusion dependency | On the Interaction of Inclusion Dependencies with Independence Atoms |

independence | Proving uniformity and independence by self-composition and coupling |

Independence atom | On the Interaction of Inclusion Dependencies with Independence Atoms |

inductive invariant | Synchronizing Constrained Horn Clauses |

infinite lists | Decidable linear list constraints |

interactive theorem proving | Formally Proving the Boolean Pythagorean Triples Conjecture |

interpolation | First-Order Interpolation and Interpolating Proof Systems |

interpretations | Higher order interpretation for higher order complexity |

Isabelle/HOL | Reasoning about Translation Lookaside Buffers |

L |

linear arithmetic | Decidable linear list constraints |

linear logic | Deep Proof Search in MELL A uniform framework for substructural logics with modalities |

linear nested sequents | A uniform framework for substructural logics with modalities |

Linear Temporal Logic | A One-Pass Tree-Shaped Tableau for LTL+Past |

linearization | Synchronizing Constrained Horn Clauses |

logic of bunched implications | Bunched Hypersequent Calculi for Distributive Substructural Logics |

logical frameworks | A uniform framework for substructural logics with modalities |

LTL | Gödel logics and the fully boxed fragment of LTL |

LTL to automata translation | Seminator: A Tool for Semi-Determinization of Omega-Automata |

M |

machine learning | TacticToe: Learning to Reason with HOL4 Tactics |

maximum independent set | From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes |

MELL | Deep Proof Search in MELL |

Memory Management Unit | Reasoning about Translation Lookaside Buffers |

memory models | Quantified Heap Invariants for Object-Oriented Programs |

model checking | Automated analysis of Stateflow models |

model expansion | Propagators and Solvers for the Algebra of Modular Systems |

modular systems | Propagators and Solvers for the Algebra of Modular Systems |

monadic fragment | Gödel logics and the fully boxed fragment of LTL |

multimodalities | A uniform framework for substructural logics with modalities |

N |

nondeterminism | Deep Proof Search in MELL |

O |

omega-automata | Seminator: A Tool for Semi-Determinization of Omega-Automata |

Operating Systems | Reasoning about Translation Lookaside Buffers |

Overlapping Rewrite Systems | Parallel Graph Rewriting with Overlapping Rules |

P |

Parallel Rewriting | Parallel Graph Rewriting with Overlapping Rules |

Partial Model Checking | A Quantitative Partial Model-Checking Function and Its Optimisation |

Past Operators | A One-Pass Tree-Shaped Tableau for LTL+Past |

Preprocessing | Blocked Clauses in First-Order Logic |

probabilistic programs | Proving uniformity and independence by self-composition and coupling |

program analysis | Cauliflower: a Solver Generator for Context-Free Language Reachability |

program verification | Proving uniformity and independence by self-composition and coupling Reasoning about Translation Lookaside Buffers |

proof assistant | Coq without Type Casts: A Complete Proof of Coq Modulo Theory |

proof automation | TacticToe: Learning to Reason with HOL4 Tactics |

proof search | Deep Proof Search in MELL |

proof theory | Deep Proof Search in MELL |

propagators | Propagators and Solvers for the Algebra of Modular Systems |

propositional satisfiability | From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes |

Q |

quantitative reasoning | A Quantitative Partial Model-Checking Function and Its Optimisation |

R |

Reasoner | RACCOON: A Connection Reasoner for the Description Logic ALC |

relational logic | Proving uniformity and independence by self-composition and coupling |

relational verification | Synchronizing Constrained Horn Clauses |

Resolution Calculus | First-Order Interpolation and Interpolating Proof Systems |

resource types | Decidable linear list constraints |

S |

SAT | Blocked Clauses in First-Order Logic |

SAT solving | Towards a Semantics of Unsatisfiability Proofs with Inprocessing |

Semantical Embedding | Theorem Provers For Every Normal Modal Logic |

semi-deterministic automata | Seminator: A Tool for Semi-Determinization of Omega-Automata |

semiring | A Quantitative Partial Model-Checking Function and Its Optimisation |

separation logic | Bunched Hypersequent Calculi for Distributive Substructural Logics |

serious games | Quantified Boolean Formulas: Call the Plumber! |

software model checking | Quantified Heap Invariants for Object-Oriented Programs |

solvers | Propagators and Solvers for the Algebra of Modular Systems |

soundness | Coq without Type Casts: A Complete Proof of Coq Modulo Theory |

Stateflow | Automated analysis of Stateflow models |

structural rules | Bunched Hypersequent Calculi for Distributive Substructural Logics |

superposition | First-Order Interpolation and Interpolating Proof Systems |

T |

tableaux | A One-Pass Tree-Shaped Tableau for LTL+Past |

term rewriting | Analyzing Runtime Complexity via Innermost Runtime Complexity |

theorem proving | Deep Network Guided Proof Search Reasoning about Translation Lookaside Buffers |

Tractable classes | From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes |

Translation Lookaside Buffer | Reasoning about Translation Lookaside Buffers |

type theory | Coq without Type Casts: A Complete Proof of Coq Modulo Theory |

U |

Unbounded Model Checking | Synchronizing Constrained Horn Clauses |

uniformity | Proving uniformity and independence by self-composition and coupling |