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