| 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 |
