EasyChair Publications
PAAR-2012 Volume Information
Volume:Pascal Fontaine, Renate A. Schmidt and Stephan Schulz (editors)
PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning

PAAR-2012 Volume Information

Title:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Editors:Pascal Fontaine, Renate A. Schmidt and Stephan Schulz
Series:EPiC Series in Computing
Publication date:August 19, 2013


Armin BierePractical Aspects of SAT Solving1
Boris MotikBuilding an Efficient OWL 2 DL Reasoner2
Jesse AlamaEscape to Mizar from ATPs3-11
Christoph Benzmüller, Jens Otten and Thomas RathsImplementing Different Proof Calculi for First-order Modal Logics12-18
Diego Caminha B de Oliveira and David MonniauxExperiments on the feasibility of using a floating-point simplex in an SMT solver19-28
Jason Crampton, Michael Huth and Jim Huan-Pu KuoAuthorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning29-42
Rajeev Gore and Jimmy ThomsonBDD-based automated reasoning in propositional non-classical logics: progress report43-57
Md Zahidul Islam and Wendy MacCaullA One-Pass Tableau-Based Workflow Verification Framework58-71
Cezary Kaliszyk and Josef UrbanInitial Experiments with External Provers and Premise Selection on HOL Light Corpora72-81
Daniel Kuehlwein and Josef UrbanLearning from Multiple Proofs: First Experiments82-94
Alexander Leitsch and Tomer LibalA Resolution Calculus for Second-order Logic with Eager Unification95
Tianyi Liang and Cesare TinelliExploiting parallelism in the ME calculus96-108
Stefan Minica, Mohammad Khodadadi, Renate A. Schmidt and Dmitry TishkovskySynthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics109-123
Anthony Monnet and Roger VillemaireCDCL with Less Destructive Backtracking through Partial Ordering124-138
Martina Seidl, Florian Lonsing and Armin Biereqbf2epr: A Tool for Generating EPR Formulas from QBF139-148
Dmitry Tishkovsky, Renate A. Schmidt and Mohammad KhodadadiMetTeL2: Towards a Tableau Prover Generation Platform149-162
Christoph Weidenbach and Patrick WischnewskiSatisfiability Checking and Query Answering for Large Ontologies163-177


8automated reasoning
3automated theorem proving
2binary decision diagrams, cdcl, interactive theorem proving, mizar, premise selection, propositional reasoning, satisfiability
1authorization enforcement functions, automated reasoning in non classical logics, bounded unification, ctl, decidable unification problems, dynamic epistemic logic of questions, effectively propositional logic, efficient second order theorem proving, encoding, epr, evaluation, first order reasoning, floating point, formal verification, hermit, higher order resolution, hol light, implementation of provers, instantiation based calculi, interrogative epistemic logic, logic, ltl model checking, machine learning, mettel2, modal logic, model checking, model evolution, mu calculus, multiple proofs, natural deduction, non classical logics, one pass tableau, ontology, ontology reasoning, owl, parallel theorem proving, partial order, progress report, proof transformation, qbf, quantified boolean formulas, query answering, regular expressions, resolution, sat, sat solving, satisfiability checking, satisfiability modulo theories, simplex, smt solving, superposition, system description, tableau, tableau calculus, tableau decision procedure, tableau prover generator, tableau synthesis framework, workflow, workflow systems