LPAR-21:Keyword Index

KeywordPapers
A
A* proof searchTacticToe: Learning to Reason with HOL4 Tactics
ALCRACCOON: A Connection Reasoner for the Description Logic ALC
algebraPropagators and Solvers for the Algebra of Modular Systems
automated complexity analysisAnalyzing Runtime Complexity via Innermost Runtime Complexity
automated reasoningBlocked Clauses in First-Order Logic
TacticToe: Learning to Reason with HOL4 Tactics
RACCOON: A Connection Reasoner for the Description Logic ALC
automated theorem provingTheorem Provers For Every Normal Modal Logic
Blocked Clauses in First-Order Logic
axiomatizationOn the Interaction of Inclusion Dependencies with Independence Atoms
B
basic feasible functionalsHigher order interpretation for higher order complexity
BBIBunched Hypersequent Calculi for Distributive Substructural Logics
blocked clausesBlocked Clauses in First-Order Logic
Towards a Semantics of Unsatisfiability Proofs with Inprocessing
Boolean Pythagorean Triples problemFormally Proving the Boolean Pythagorean Triples Conjecture
bunched calculiBunched Hypersequent Calculi for Distributive Substructural Logics
C
clause eliminationBlocked Clauses in First-Order Logic
complexityOn the Interaction of Inclusion Dependencies with Independence Atoms
computational complexityQuantified Boolean Formulas: Call the Plumber!
Confluent Rewrite RelationsParallel Graph Rewriting with Overlapping Rules
connection methodRACCOON: A Connection Reasoner for the Description Logic ALC
Constrained Horn ClausesSynchronizing Constrained Horn Clauses
constraint satisfactionDecidable linear list constraints
context-free languagesCauliflower: a Solver Generator for Context-Free Language Reachability
continuation-passing styleAutomated analysis of Stateflow models
CoqCoq without Type Casts: A Complete Proof of Coq Modulo Theory
cut eliminationBunched Hypersequent Calculi for Distributive Substructural Logics
D
deep inferenceDeep Proof Search in MELL
deep learningDeep Network Guided Proof Search
Description LogicRACCOON: A Connection Reasoner for the Description Logic ALC
distributive substructural logicsBunched Hypersequent Calculi for Distributive Substructural Logics
DRAT proofsTowards a Semantics of Unsatisfiability Proofs with Inprocessing
Dunn-Mints calculiBunched Hypersequent Calculi for Distributive Substructural Logics
E
educational logic softwareQuantified Boolean Formulas: Call the Plumber!
evaluation strategiesAnalyzing Runtime Complexity via Innermost Runtime Complexity
F
first-order logicBlocked Clauses in First-Order Logic
Deep Network Guided Proof Search
first-order theoryCoq without Type Casts: A Complete Proof of Coq Modulo Theory
formal proofsFormally Proving the Boolean Pythagorean Triples Conjecture
G
graph reachabilityCauliflower: a Solver Generator for Context-Free Language Reachability
graph rewritingParallel Graph Rewriting with Overlapping Rules
Gödel logicGödel logics and the fully boxed fragment of LTL
H
Higher-order complexityHigher order interpretation for higher order complexity
higher-order logicTheorem Provers For Every Normal Modal Logic
TacticToe: Learning to Reason with HOL4 Tactics
Higher-Order Modal LogicTheorem Provers For Every Normal Modal Logic
Horn Clause SolvingQuantified Heap Invariants for Object-Oriented Programs
hypersequentsBunched Hypersequent Calculi for Distributive Substructural Logics
I
implication problemOn the Interaction of Inclusion Dependencies with Independence Atoms
inclusion dependencyOn the Interaction of Inclusion Dependencies with Independence Atoms
independenceProving uniformity and independence by self-composition and coupling
Independence atomOn the Interaction of Inclusion Dependencies with Independence Atoms
inductive invariantSynchronizing Constrained Horn Clauses
infinite listsDecidable linear list constraints
interactive theorem provingFormally Proving the Boolean Pythagorean Triples Conjecture
interpolationFirst-Order Interpolation and Interpolating Proof Systems
interpretationsHigher order interpretation for higher order complexity
Isabelle/HOLReasoning about Translation Lookaside Buffers
L
linear arithmeticDecidable linear list constraints
linear logicDeep Proof Search in MELL
A uniform framework for substructural logics with modalities
linear nested sequentsA uniform framework for substructural logics with modalities
Linear Temporal LogicA One-Pass Tree-Shaped Tableau for LTL+Past
linearizationSynchronizing Constrained Horn Clauses
logic of bunched implicationsBunched Hypersequent Calculi for Distributive Substructural Logics
logical frameworksA uniform framework for substructural logics with modalities
LTLGödel logics and the fully boxed fragment of LTL
LTL to automata translationSeminator: A Tool for Semi-Determinization of Omega-Automata
M
machine learningTacticToe: Learning to Reason with HOL4 Tactics
maximum independent setFrom SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes
MELLDeep Proof Search in MELL
Memory Management UnitReasoning about Translation Lookaside Buffers
memory modelsQuantified Heap Invariants for Object-Oriented Programs
model checkingAutomated analysis of Stateflow models
model expansionPropagators and Solvers for the Algebra of Modular Systems
modular systemsPropagators and Solvers for the Algebra of Modular Systems
monadic fragmentGödel logics and the fully boxed fragment of LTL
multimodalitiesA uniform framework for substructural logics with modalities
N
nondeterminismDeep Proof Search in MELL
O
omega-automataSeminator: A Tool for Semi-Determinization of Omega-Automata
Operating SystemsReasoning about Translation Lookaside Buffers
Overlapping Rewrite SystemsParallel Graph Rewriting with Overlapping Rules
P
Parallel RewritingParallel Graph Rewriting with Overlapping Rules
Partial Model CheckingA Quantitative Partial Model-Checking Function and Its Optimisation
Past OperatorsA One-Pass Tree-Shaped Tableau for LTL+Past
PreprocessingBlocked Clauses in First-Order Logic
probabilistic programsProving uniformity and independence by self-composition and coupling
program analysisCauliflower: a Solver Generator for Context-Free Language Reachability
program verificationProving uniformity and independence by self-composition and coupling
Reasoning about Translation Lookaside Buffers
proof assistantCoq without Type Casts: A Complete Proof of Coq Modulo Theory
proof automationTacticToe: Learning to Reason with HOL4 Tactics
proof searchDeep Proof Search in MELL
proof theoryDeep Proof Search in MELL
propagatorsPropagators and Solvers for the Algebra of Modular Systems
propositional satisfiabilityFrom SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes
Q
quantitative reasoningA Quantitative Partial Model-Checking Function and Its Optimisation
R
ReasonerRACCOON: A Connection Reasoner for the Description Logic ALC
relational logicProving uniformity and independence by self-composition and coupling
relational verificationSynchronizing Constrained Horn Clauses
Resolution CalculusFirst-Order Interpolation and Interpolating Proof Systems
resource typesDecidable linear list constraints
S
SATBlocked Clauses in First-Order Logic
SAT solvingTowards a Semantics of Unsatisfiability Proofs with Inprocessing
Semantical EmbeddingTheorem Provers For Every Normal Modal Logic
semi-deterministic automataSeminator: A Tool for Semi-Determinization of Omega-Automata
semiringA Quantitative Partial Model-Checking Function and Its Optimisation
separation logicBunched Hypersequent Calculi for Distributive Substructural Logics
serious gamesQuantified Boolean Formulas: Call the Plumber!
software model checkingQuantified Heap Invariants for Object-Oriented Programs
solversPropagators and Solvers for the Algebra of Modular Systems
soundnessCoq without Type Casts: A Complete Proof of Coq Modulo Theory
StateflowAutomated analysis of Stateflow models
structural rulesBunched Hypersequent Calculi for Distributive Substructural Logics
superpositionFirst-Order Interpolation and Interpolating Proof Systems
T
tableauxA One-Pass Tree-Shaped Tableau for LTL+Past
term rewritingAnalyzing Runtime Complexity via Innermost Runtime Complexity
theorem provingDeep Network Guided Proof Search
Reasoning about Translation Lookaside Buffers
Tractable classesFrom SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes
Translation Lookaside BufferReasoning about Translation Lookaside Buffers
type theoryCoq without Type Casts: A Complete Proof of Coq Modulo Theory
U
Unbounded Model CheckingSynchronizing Constrained Horn Clauses
uniformityProving uniformity and independence by self-composition and coupling