PAAR-2012:Keyword Index

KeywordPapers
A
Authorization Enforcement FunctionsAuthorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning
automated reasoningPractical 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 logicsImplementing Different Proof Calculi for First-order Modal Logics
automated theorem provingEscape to Mizar from ATPs
Implementing Different Proof Calculi for First-order Modal Logics
Learning from Multiple Proofs: First Experiments
B
Binary Decision DiagramsAuthorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning
BDD-based automated reasoning in propositional non-classical logics: progress report
Bounded unificationA Resolution Calculus for Second-order Logic with Eager Unification
C
CDCLPractical Aspects of SAT Solving
CDCL with Less Destructive Backtracking through Partial Ordering
CTLA One-Pass Tableau-Based Workflow Verification Framework
D
Decidable unification problemsA Resolution Calculus for Second-order Logic with Eager Unification
Dynamic Epistemic Logic of QuestionsSynthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics
E
Effectively Propositional Logicqbf2epr: A Tool for Generating EPR Formulas from QBF
Efficient second-order theorem provingA Resolution Calculus for Second-order Logic with Eager Unification
encodingqbf2epr: A Tool for Generating EPR Formulas from QBF
EPRqbf2epr: A Tool for Generating EPR Formulas from QBF
evaluationImplementing Different Proof Calculi for First-order Modal Logics
F
first-order reasoningSatisfiability Checking and Query Answering for Large Ontologies
floating-pointExperiments on the feasibility of using a floating-point simplex in an SMT solver
formal verificationA One-Pass Tableau-Based Workflow Verification Framework
H
HERMITBuilding an Efficient OWL 2 DL Reasoner
Higher-order resolutionA Resolution Calculus for Second-order Logic with Eager Unification
HOL LightInitial Experiments with External Provers and Premise Selection on HOL Light Corpora
I
implementation of proversImplementing Different Proof Calculi for First-order Modal Logics
Instantiation-based calculiExploiting parallelism in the ME calculus
interactive theorem provingEscape to Mizar from ATPs
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora
Interrogative Epistemic LogicSynthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics
L
logicMetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform
LTL model checkingAuthorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning
M
machine learningLearning from Multiple Proofs: First Experiments
Mettel2Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics
MizarEscape to Mizar from ATPs
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora
modal logicImplementing Different Proof Calculi for First-order Modal Logics
model checkingA One-Pass Tableau-Based Workflow Verification Framework
Model EvolutionExploiting parallelism in the ME calculus
mu-calculusBDD-based automated reasoning in propositional non-classical logics: progress report
multiple proofsLearning from Multiple Proofs: First Experiments
N
natural deductionEscape to Mizar from ATPs
non-classical logicsBDD-based automated reasoning in propositional non-classical logics: progress report
O
one-pass tableauA One-Pass Tableau-Based Workflow Verification Framework
OntologyBuilding an Efficient OWL 2 DL Reasoner
Ontology ReasoningSatisfiability Checking and Query Answering for Large Ontologies
OWLBuilding an Efficient OWL 2 DL Reasoner
P
parallel theorem provingExploiting parallelism in the ME calculus
partial orderCDCL with Less Destructive Backtracking through Partial Ordering
premise selectionInitial Experiments with External Provers and Premise Selection on HOL Light Corpora
Learning from Multiple Proofs: First Experiments
Progress ReportBDD-based automated reasoning in propositional non-classical logics: progress report
proof transformationEscape to Mizar from ATPs
propositional reasoningPractical Aspects of SAT Solving
CDCL with Less Destructive Backtracking through Partial Ordering
Q
QBFqbf2epr: A Tool for Generating EPR Formulas from QBF
Quantified Boolean Formulasqbf2epr: A Tool for Generating EPR Formulas from QBF
query answeringSatisfiability Checking and Query Answering for Large Ontologies
R
regular expressionsA Resolution Calculus for Second-order Logic with Eager Unification
resolutionEscape to Mizar from ATPs
S
SATCDCL with Less Destructive Backtracking through Partial Ordering
SAT solvingPractical Aspects of SAT Solving
satisfiabilityPractical Aspects of SAT Solving
Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning
satisfiability checkingSatisfiability Checking and Query Answering for Large Ontologies
Satisfiability Modulo TheoriesExperiments on the feasibility of using a floating-point simplex in an SMT solver
simplexExperiments on the feasibility of using a floating-point simplex in an SMT solver
SMT solvingExperiments on the feasibility of using a floating-point simplex in an SMT solver
superpositionSatisfiability Checking and Query Answering for Large Ontologies
system descriptionMetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform
T
TableauBuilding an Efficient OWL 2 DL Reasoner
tableau calculusMetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform
tableau decision procedureMetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform
tableau prover generatorMetTeL<sup>2</sup>: Towards a Tableau Prover Generation Platform
tableau synthesis frameworkSynthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics
W
workflowA One-Pass Tableau-Based Workflow Verification Framework
Workflow SystemsAuthorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning