A |

Ad-hoc overloading | A Mechanised Semantics for HOL with Ad-hoc Overloading |

AI heuristics | Decision levels are stable: towards better SAT heuristics |

alternating Turing machines | Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard |

Analysis by simulation | A compositional semantics for Repairable Fault Trees with general distributions |

Answer Set Programming | An ASP-based Approach for Boolean Networks Representation and Attractor Detection |

antiprenexing | Antiprenexing for WSkS: A Little Goes a Long Way |

attractors | An ASP-based Approach for Boolean Networks Representation and Attractor Detection |

automata | Antiprenexing for WSkS: A Little Goes a Long Way |

automated reasoning | Decision levels are stable: towards better SAT heuristics |

automated theorem proving | Stateful Premise Selection by Recurrent Neural Networks |

axiomatisation | Models of Concurrent Kleene Algebra |

B |

Bioinformatics | An ASP-based Approach for Boolean Networks Representation and Attractor Detection |

Boolean networks | An ASP-based Approach for Boolean Networks Representation and Attractor Detection |

Boolean satisfiability | Finding Periodic Apartments via Boolean Satisfiability and Orderly Generation |

Boolean Sensitivity | Sensitivity Analysis of Locked Circuits |

C |

CDCL | A Verified SAT Solver Framework including Optimization and Partial Valuations |

CDCL with branch and bound | A Verified SAT Solver Framework including Optimization and Partial Valuations |

chromatic number of the plane | Coloring Unit-Distance Strips using SAT |

clauses | NACRE - A Nogood And Clause Reasoning Engine |

combinators | Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic |

common knowledge | Learning What Others Know |

communication | Learning What Others Know |

completeness | Models of Concurrent Kleene Algebra |

complexity | Finding Small Proofs for Description Logic Entailments: Theory and Practice Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard |

computer mathematics | Finding Periodic Apartments via Boolean Satisfiability and Orderly Generation |

Concurrent Kleene Algebra | Models of Concurrent Kleene Algebra |

Constraint Programming | NACRE - A Nogood And Clause Reasoning Engine |

constraint solving | Decision levels are stable: towards better SAT heuristics |

Coq | Tactic Learning and Proving for the Coq Proof Assistant |

D |

data structures | Learning Data Structure Shapes from Memory Graphs |

decidability | Polynomial Loops: Beyond Termination |

decision procedure | Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions |

Deep Neural Networks | Minimal Modifications of Deep Neural Networks using Verification |

deep neural networks modification | Minimal Modifications of Deep Neural Networks using Verification |

Description Logic | Finding Small Proofs for Description Logic Entailments: Theory and Practice |

diagnosis | Rotation Based MSS/MCS Enumeration |

Diophantine equations | Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic |

distributed knowledge | Learning What Others Know |

DRAT proofs | RAT Elimination |

Dynamic Fault Trees | A compositional semantics for Repairable Fault Trees with general distributions |

dynamic logic | Learning What Others Know |

E |

electronic circuits | Sensitivity Analysis of Locked Circuits |

epistemic logic | Learning What Others Know |

equivalence | Induction Models on $\mathbb{N}$ |

explanation | Finding Small Proofs for Description Logic Entailments: Theory and Practice |

F |

Fault Tree Analysis | A compositional semantics for Repairable Fault Trees with general distributions |

functional programming languages | A typed parallel lambda-calculus via 1-depth intermediate proofs |

G |

graph coloring | Coloring Unit-Distance Strips using SAT |

Gromov's subgroup conjecture | Finding Periodic Apartments via Boolean Satisfiability and Orderly Generation |

guarded fragment | The Triguarded Fragment with Transitivity |

H |

halting problem | Polynomial Loops: Beyond Termination |

higher-order logic | A Mechanised Semantics for HOL with Ad-hoc Overloading |

HOL | Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic |

hypersequent calculi | A typed parallel lambda-calculus via 1-depth intermediate proofs |

I |

induction | Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard |

Induction Models | Induction Models on $\mathbb{N}$ |

Infeasibility analysis | Rotation Based MSS/MCS Enumeration |

information flow security | Parameter Synthesis for Probabilistic Hyperproperties |

information sharing | Learning What Others Know |

Input/Output Stochastic Automata | A compositional semantics for Repairable Fault Trees with general distributions |

interactive theorem proving | Tactic Learning and Proving for the Coq Proof Assistant A Mechanised Semantics for HOL with Ad-hoc Overloading |

intermediate logics | A typed parallel lambda-calculus via 1-depth intermediate proofs |

K |

Knowledge Access | On Reasoning about Access to Knowledge |

Knowledge Hiding | On Reasoning about Access to Knowledge |

knowledge sharing | On Reasoning about Access to Knowledge |

L |

lambda calculus | A typed parallel lambda-calculus via 1-depth intermediate proofs |

litmus test | Models of Concurrent Kleene Algebra |

Logic Locking | Sensitivity Analysis of Locked Circuits |

logic programming | Decision levels are stable: towards better SAT heuristics An ASP-based Approach for Boolean Networks Representation and Attractor Detection |

M |

machine learning | Tactic Learning and Proving for the Coq Proof Assistant Stateful Premise Selection by Recurrent Neural Networks |

Mathematical Induction | Induction Models on $\mathbb{N}$ |

Maximal satisfiable subsets | Rotation Based MSS/MCS Enumeration |

MCS | Rotation Based MSS/MCS Enumeration |

Minimal Correction Subsets | Rotation Based MSS/MCS Enumeration |

MSS | Rotation Based MSS/MCS Enumeration |

N |

natural deduction | A typed parallel lambda-calculus via 1-depth intermediate proofs |

neural networks verification | Minimal Modifications of Deep Neural Networks using Verification |

neural networks watermarking | Minimal Modifications of Deep Neural Networks using Verification |

nogoods | NACRE - A Nogood And Clause Reasoning Engine |

O |

orderly generation | Finding Periodic Apartments via Boolean Satisfiability and Orderly Generation |

P |

Partial Function Model | Models of Concurrent Kleene Algebra |

Preprocessing | Antiprenexing for WSkS: A Little Goes a Long Way |

probabilistic systems | Parameter Synthesis for Probabilistic Hyperproperties |

Prolog | Learning Data Structure Shapes from Memory Graphs |

Proof synthesis | Tactic Learning and Proving for the Coq Proof Assistant |

Proof-based interpolation | RAT Elimination |

proofs | Finding Small Proofs for Description Logic Entailments: Theory and Practice |

propositional logic | RAT Elimination On Reasoning about Access to Knowledge |

R |

Recurrent Neural Networks | Stateful Premise Selection by Recurrent Neural Networks |

reduction | Induction Models on $\mathbb{N}$ |

Reinforcement Learning | Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic |

Repairable Fault Trees | A compositional semantics for Repairable Fault Trees with general distributions |

Runtime Complexity | Polynomial Loops: Beyond Termination |

S |

SAT | NACRE - A Nogood And Clause Reasoning Engine |

SAT solving | Coloring Unit-Distance Strips using SAT RAT Elimination |

SAT/SMT | Decision levels are stable: towards better SAT heuristics |

satisfiability | Sensitivity Analysis of Locked Circuits |

satisfiability problem | The Triguarded Fragment with Transitivity |

semantic model | A compositional semantics for Repairable Fault Trees with general distributions |

separation logic | Learning Data Structure Shapes from Memory Graphs Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions |

shape predicates | Learning Data Structure Shapes from Memory Graphs |

solver | NACRE - A Nogood And Clause Reasoning Engine |

synthesis | Parameter Synthesis for Probabilistic Hyperproperties |

T |

Tactic Search | Tactic Learning and Proving for the Coq Proof Assistant |

termination | Polynomial Loops: Beyond Termination |

transitive relations | The Triguarded Fragment with Transitivity |

tree neural networks | Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic |

triguarded fragment | The Triguarded Fragment with Transitivity |

two-variable fragment | The Triguarded Fragment with Transitivity |

type theory | A typed parallel lambda-calculus via 1-depth intermediate proofs |

U |

undecidability | Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions |

V |

verification | A Verified SAT Solver Framework including Optimization and Partial Valuations Minimal Modifications of Deep Neural Networks using Verification |

W |

Weak determinism | A compositional semantics for Repairable Fault Trees with general distributions |

weak monadic second-order logic | Antiprenexing for WSkS: A Little Goes a Long Way |

WSkS | Antiprenexing for WSkS: A Little Goes a Long Way |