|  | 
|  | 
| | PAAR-2012: Author Index| Author | Papers | 
|---|
 | A |  | Alama, Jesse | Escape to Mizar from ATPs |  | B |  | Benzmüller, Christoph | Implementing Different Proof Calculi for First-order Modal Logics |  | Biere, Armin | Practical Aspects of SAT Solving qbf2epr: A Tool for Generating EPR Formulas from QBF
 |  | C |  | Caminha B de Oliveira, Diego | Experiments on the feasibility of using a floating-point simplex in an SMT solver |  | Crampton, Jason | Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning |  | G |  | Gore, Rajeev | BDD-based automated reasoning in propositional non-classical logics: progress report |  | H |  | Huth, Michael | Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning |  | I |  | Islam, Md Zahidul | A One-Pass Tableau-Based Workflow Verification Framework |  | K |  | Kaliszyk, Cezary | Initial Experiments with External Provers and Premise Selection on HOL Light Corpora |  | Khodadadi, Mohammad | Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics MetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform
 |  | Kuehlwein, Daniel | Learning from Multiple Proofs: First Experiments |  | Kuo, Jim Huan-Pu | Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning |  | L |  | Leitsch, Alexander | A Resolution Calculus for Second-order Logic with Eager Unification |  | Liang, Tianyi | Exploiting parallelism in the ME calculus |  | Libal, Tomer | A Resolution Calculus for Second-order Logic with Eager Unification |  | Lonsing, Florian | qbf2epr: A Tool for Generating EPR Formulas from QBF |  | M |  | MacCaull, Wendy | A One-Pass Tableau-Based Workflow Verification Framework |  | Minica, Stefan | Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics |  | Monnet, Anthony | CDCL with Less Destructive Backtracking through Partial Ordering |  | Monniaux, David | Experiments on the feasibility of using a floating-point simplex in an SMT solver |  | Motik, Boris | Building an Efficient OWL 2 DL Reasoner |  | O |  | Otten, Jens | Implementing Different Proof Calculi for First-order Modal Logics |  | R |  | Raths, Thomas | Implementing Different Proof Calculi for First-order Modal Logics |  | S |  | Schmidt, Renate A. | Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics MetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform
 |  | Seidl, Martina | qbf2epr: A Tool for Generating EPR Formulas from QBF |  | T |  | Thomson, Jimmy | BDD-based automated reasoning in propositional non-classical logics: progress report |  | Tinelli, Cesare | Exploiting parallelism in the ME calculus |  | Tishkovsky, Dmitry | Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics MetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform
 |  | U |  | Urban, Josef | Initial Experiments with External Provers and Premise Selection on HOL Light Corpora Learning from Multiple Proofs: First Experiments
 |  | V |  | Villemaire, Roger | CDCL with Less Destructive Backtracking through Partial Ordering |  | W |  | Weidenbach, Christoph | Satisfiability Checking and Query Answering for Large Ontologies |  | Wischnewski, Patrick | Satisfiability Checking and Query Answering for Large Ontologies | 
 | 
 | 
|