Abstract is missing.
- Practical Aspects of SAT SolvingArmin Biere. 1 [doi]
- Building an Efficient OWL 2 DL ReasonerBoris Motik. 2 [doi]
- Escape to Mizar from ATPsJesse Alama. 3-11 [doi]
- Implementing Different Proof Calculi for First-order Modal LogicsChristoph Benzmüller, Jens Otten, Thomas Raths. 12-18 [doi]
- Experiments on the feasibility of using a floating-point simplex in an SMT solverDiego Caminha B. de Oliveira, David Monniaux. 19-28 [doi]
- Authorization Enforcement in Workflows: Maintaining Realizability Via Automated ReasoningJason Crampton, Michael Huth, Jim Huan-Pu Kuo. 29-42 [doi]
- BDD-based automated reasoning in propositional non-classical logics: progress reportRajeev Goré, Jimmy Thomson. 43-57 [doi]
- A One-Pass Tableau-Based Workflow Verification FrameworkMd. Zahidul Islam, Wendy MacCaull. 58-71 [doi]
- Initial Experiments with External Provers and Premise Selection on HOL Light CorporaCezary Kaliszyk, Josef Urban. 72-81 [doi]
- Learning from Multiple Proofs: First ExperimentsDaniel Kühlwein, Josef Urban. 82-94 [doi]
- A Resolution Calculus for Second-order Logic with Eager UnificationAlexander Leitsch, Tomer Libal. 95 [doi]
- Exploiting parallelism in the ME calculusTianyi Liang, Cesare Tinelli. 96-108 [doi]
- Synthesising and Implementing Tableau Calculi for Interrogative Epistemic LogicsStefan Minica, Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky. 109-123 [doi]
- CDCL with Less Destructive Backtracking through Partial OrderingAnthony Monnet, Roger Villemaire. 124-138 [doi]
- qbf2epr: A Tool for Generating EPR Formulas from QBFMartina Seidl, Florian Lonsing, Armin Biere. 139-148 [doi]
- 2: Towards a Tableau Prover Generation PlatformDmitry Tishkovsky, Renate A. Schmidt, Mohammad Khodadadi. 149-162 [doi]
- Satisfiability Checking and Query Answering for Large OntologiesChristoph Weidenbach, Patrick Wischnewski. 163-177 [doi]