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