A |

Authorization Enforcement Functions | Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning |

automated reasoning | Practical Aspects of SAT Solving Building an Efficient OWL 2 DL Reasoner Escape to Mizar from ATPs Experiments on the feasibility of using a floating-point simplex in an SMT solver BDD-based automated reasoning in propositional non-classical logics: progress report Initial Experiments with External Provers and Premise Selection on HOL Light Corpora Learning from Multiple Proofs: First Experiments CDCL with Less Destructive Backtracking through Partial Ordering |

automated reasoning in non-classical logics | Implementing Different Proof Calculi for First-order Modal Logics |

automated theorem proving | Escape to Mizar from ATPs Implementing Different Proof Calculi for First-order Modal Logics Learning from Multiple Proofs: First Experiments |

B |

Binary Decision Diagrams | Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning BDD-based automated reasoning in propositional non-classical logics: progress report |

Bounded unification | A Resolution Calculus for Second-order Logic with Eager Unification |

C |

CDCL | Practical Aspects of SAT Solving CDCL with Less Destructive Backtracking through Partial Ordering |

CTL | A One-Pass Tableau-Based Workflow Verification Framework |

D |

Decidable unification problems | A Resolution Calculus for Second-order Logic with Eager Unification |

Dynamic Epistemic Logic of Questions | Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics |

E |

Effectively Propositional Logic | qbf2epr: A Tool for Generating EPR Formulas from QBF |

Efficient second-order theorem proving | A Resolution Calculus for Second-order Logic with Eager Unification |

encoding | qbf2epr: A Tool for Generating EPR Formulas from QBF |

EPR | qbf2epr: A Tool for Generating EPR Formulas from QBF |

evaluation | Implementing Different Proof Calculi for First-order Modal Logics |

F |

first-order reasoning | Satisfiability Checking and Query Answering for Large Ontologies |

floating-point | Experiments on the feasibility of using a floating-point simplex in an SMT solver |

formal verification | A One-Pass Tableau-Based Workflow Verification Framework |

H |

HERMIT | Building an Efficient OWL 2 DL Reasoner |

Higher-order resolution | A Resolution Calculus for Second-order Logic with Eager Unification |

HOL Light | Initial Experiments with External Provers and Premise Selection on HOL Light Corpora |

I |

implementation of provers | Implementing Different Proof Calculi for First-order Modal Logics |

Instantiation-based calculi | Exploiting parallelism in the ME calculus |

interactive theorem proving | Escape to Mizar from ATPs Initial Experiments with External Provers and Premise Selection on HOL Light Corpora |

Interrogative Epistemic Logic | Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics |

L |

logic | MetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform |

LTL model checking | Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning |

M |

machine learning | Learning from Multiple Proofs: First Experiments |

Mettel2 | Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics |

Mizar | Escape to Mizar from ATPs Initial Experiments with External Provers and Premise Selection on HOL Light Corpora |

modal logic | Implementing Different Proof Calculi for First-order Modal Logics |

model checking | A One-Pass Tableau-Based Workflow Verification Framework |

Model Evolution | Exploiting parallelism in the ME calculus |

mu-calculus | BDD-based automated reasoning in propositional non-classical logics: progress report |

multiple proofs | Learning from Multiple Proofs: First Experiments |

N |

natural deduction | Escape to Mizar from ATPs |

non-classical logics | BDD-based automated reasoning in propositional non-classical logics: progress report |

O |

one-pass tableau | A One-Pass Tableau-Based Workflow Verification Framework |

Ontology | Building an Efficient OWL 2 DL Reasoner |

Ontology Reasoning | Satisfiability Checking and Query Answering for Large Ontologies |

OWL | Building an Efficient OWL 2 DL Reasoner |

P |

parallel theorem proving | Exploiting parallelism in the ME calculus |

partial order | CDCL with Less Destructive Backtracking through Partial Ordering |

premise selection | Initial Experiments with External Provers and Premise Selection on HOL Light Corpora Learning from Multiple Proofs: First Experiments |

Progress Report | BDD-based automated reasoning in propositional non-classical logics: progress report |

proof transformation | Escape to Mizar from ATPs |

propositional reasoning | Practical Aspects of SAT Solving CDCL with Less Destructive Backtracking through Partial Ordering |

Q |

QBF | qbf2epr: A Tool for Generating EPR Formulas from QBF |

Quantified Boolean Formulas | qbf2epr: A Tool for Generating EPR Formulas from QBF |

query answering | Satisfiability Checking and Query Answering for Large Ontologies |

R |

regular expressions | A Resolution Calculus for Second-order Logic with Eager Unification |

resolution | Escape to Mizar from ATPs |

S |

SAT | CDCL with Less Destructive Backtracking through Partial Ordering |

SAT solving | Practical Aspects of SAT Solving |

satisfiability | Practical Aspects of SAT Solving Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning |

satisfiability checking | Satisfiability Checking and Query Answering for Large Ontologies |

Satisfiability Modulo Theories | Experiments on the feasibility of using a floating-point simplex in an SMT solver |

simplex | Experiments on the feasibility of using a floating-point simplex in an SMT solver |

SMT solving | Experiments on the feasibility of using a floating-point simplex in an SMT solver |

superposition | Satisfiability Checking and Query Answering for Large Ontologies |

system description | MetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform |

T |

Tableau | Building an Efficient OWL 2 DL Reasoner |

tableau calculus | MetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform |

tableau decision procedure | MetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform |

tableau prover generator | MetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform |

tableau synthesis framework | Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics |

W |

workflow | A One-Pass Tableau-Based Workflow Verification Framework |

Workflow Systems | Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning |