LPAR-21: 21ST INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

This page contains an index consisting of author-provided keywords.

A
A* proof search	TacticToe: Learning to Reason with HOL4 Tactics
Abduction	Abduction by Non-Experts
ALC	RACCOON: A Connection Reasoner for the Description Logic ALC
algebra	Propagators and Solvers for the Algebra of Modular Systems
Antichains	Formalization of some central theorems in combinatorics of finite sets
Antipatterns	Reasoning with Concept Diagrams about Antipatterns
automata theory	Translating C# to Branching Symbolic Transducers
automated complexity analysis	Analyzing Runtime Complexity via Innermost Runtime Complexity
automated reasoning	TacticToe: Learning to Reason with HOL4 Tactics Blocked Clauses in First-Order Logic RACCOON: A Connection Reasoner for the Description Logic ALC
automated theorem prover	Leo-III Version 1.1 (System description)
Automated Theorem Proving	Theorem Provers For Every Normal Modal Logic Blocked Clauses in First-Order Logic
axiomatization	On the Interaction of Inclusion Dependencies with Independence Atoms
B
Basic Feasible Functionals	Higher order interpretation for higher order complexity
BBI	Bunched Hypersequent Calculi for Distributive Substructural Logics
blocked clauses	Towards a Semantics of Unsatisfiability Proofs with Inprocessing Blocked Clauses in First-Order Logic
Boolean Pythagorean Triples problem	Formally Proving the Boolean Pythagorean Triples Conjecture
bunched calculi	Bunched Hypersequent Calculi for Distributive Substructural Logics
C
Chains	Formalization of some central theorems in combinatorics of finite sets
clause elimination	Blocked Clauses in First-Order Logic
complexity	On the Interaction of Inclusion Dependencies with Independence Atoms
computational complexity	Quantified Boolean Formulas: Call the Plumber!
computational complexity of reasoning	Decidability of Fair Termination of Gossip Protocols
Confluent Rewrite Relations	On Simultaneous Transformations with Overlapping Graph Rewrite Systems
connection method	RACCOON: A Connection Reasoner for the Description Logic ALC
Constrained Horn clauses	Synchronizing Constrained Horn Clauses
constraint satisfaction	Decidable linear list constraints
Context-free languages	Cauliflower: a Solver Generator for Context-Free Language Reachability
Continuation passing style	Automated analysis of Stateflow models
Coq	A complete proof of Coq modulo Theory
Crowdsourcing	Abduction by Non-Experts
cut-elimination	Bunched Hypersequent Calculi for Distributive Substructural Logics
D
deep inference	Deep Proof Search in MELL
Deep Learning	Deep Network Guided Proof Search
description logic	RACCOON: A Connection Reasoner for the Description Logic ALC
Diagrammatic Reasoning	Reasoning with Concept Diagrams about Antipatterns
Dilworth's theorem	Formalization of some central theorems in combinatorics of finite sets
distributive substructural logics	Bunched Hypersequent Calculi for Distributive Substructural Logics
domain specific language	Translating C# to Branching Symbolic Transducers
DRAT proofs	Towards a Semantics of Unsatisfiability Proofs with Inprocessing
Dunn-Mints calculi	Bunched Hypersequent Calculi for Distributive Substructural Logics
E
educational logic software	Quantified Boolean Formulas: Call the Plumber!
epistemic logic	Decidability of Fair Termination of Gossip Protocols
evaluation strategies	Analyzing Runtime Complexity via Innermost Runtime Complexity
F
fair termination	Decidability of Fair Termination of Gossip Protocols
First Order Theory	A complete proof of Coq modulo Theory
First-Order Logic	Blocked Clauses in First-Order Logic Deep Network Guided Proof Search
formal proofs	Formalization of some central theorems in combinatorics of finite sets Formally Proving the Boolean Pythagorean Triples Conjecture
G
gossip protocols	Decidability of Fair Termination of Gossip Protocols
Graph reachability	Cauliflower: a Solver Generator for Context-Free Language Reachability
Graph Rewriting	On Simultaneous Transformations with Overlapping Graph Rewrite Systems
Gödel logic	Gödel logics and the fully boxed fragment of LTL
H
Hall's theorem	Formalization of some central theorems in combinatorics of finite sets
Higher order complexity	Higher order interpretation for higher order complexity
higher-order logic	Theorem Provers For Every Normal Modal Logic TacticToe: Learning to Reason with HOL4 Tactics Leo-III Version 1.1 (System description)
Higher-Order Modal Logic	Theorem Provers For Every Normal Modal Logic
horn clause solving	Quantified Heap Invariants for Object-Oriented Programs
Horn solving	Abduction by Non-Experts
hypersequents	Bunched Hypersequent Calculi for Distributive Substructural Logics
I
implication problem	On the Interaction of Inclusion Dependencies with Independence Atoms
inclusion dependency	On the Interaction of Inclusion Dependencies with Independence Atoms
independence	Proving uniformity and independence by self-composition and coupling
independence atom	On the Interaction of Inclusion Dependencies with Independence Atoms
Inductive invariant	Synchronizing Constrained Horn Clauses
infinite lists	Decidable linear list constraints
interactive theorem proving	Formally Proving the Boolean Pythagorean Triples Conjecture
interpolation	An Interpolation-based Compiler and Optimizer for Relational Queries (System Implementation Report) First-Order Interpolation and Interpolating Proofs Systems
Interpretations	Higher order interpretation for higher order complexity
Isabelle/HOL	Reasoning about Translation Lookaside Buffers
K
knowledge based programs	Decidability of Fair Termination of Gossip Protocols
Knowledge Representation	Reasoning with Concept Diagrams about Antipatterns
L
linear arithmetic	Decidable linear list constraints
linear logic	Deep Proof Search in MELL A uniform framework for substructural logics with modalities
linear nested sequents	A uniform framework for substructural logics with modalities
Linear Temporal Logic	A One-Pass Tree-Shaped Tableau for LTL+Past
Linearization	Synchronizing Constrained Horn Clauses
logic of bunched implications	Bunched Hypersequent Calculi for Distributive Substructural Logics
logical frameworks	A uniform framework for substructural logics with modalities
LTL	Gödel logics and the fully boxed fragment of LTL
LTL to automata translation	Seminator: A Tool for Semi-Determinization of Omega-Automata
M
machine learning	TacticToe: Learning to Reason with HOL4 Tactics
Maximum independent set	From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes
MELL	Deep Proof Search in MELL
Memory Management Unit	Reasoning about Translation Lookaside Buffers
memory models	Quantified Heap Invariants for Object-Oriented Programs
Mirsky's theorems	Formalization of some central theorems in combinatorics of finite sets
Model Checking	Automated analysis of Stateflow models
model expansion	Propagators and Solvers for the Algebra of Modular Systems
modular systems	Propagators and Solvers for the Algebra of Modular Systems
monadic fragment	Gödel logics and the fully boxed fragment of LTL
multimodalities	A uniform framework for substructural logics with modalities
N
nondeterminism	Deep Proof Search in MELL
O
omega-automata	Seminator: A Tool for Semi-Determinization of Omega-Automata
Ontologies	Reasoning with Concept Diagrams about Antipatterns
Operating Systems	Reasoning about Translation Lookaside Buffers
Overlapping Rewrite Systems	On Simultaneous Transformations with Overlapping Graph Rewrite Systems
P
Parallel Rewriting	On Simultaneous Transformations with Overlapping Graph Rewrite Systems
paramodulation	Leo-III Version 1.1 (System description)
Partial Model Checking	A Quantitative Partial Model-Checking Function and Its Optimisation
Partially ordered sets	Formalization of some central theorems in combinatorics of finite sets
Past Operators	A One-Pass Tree-Shaped Tableau for LTL+Past
preprocessing	Blocked Clauses in First-Order Logic
probabilistic programs	Proving uniformity and independence by self-composition and coupling
Program analysis	Cauliflower: a Solver Generator for Context-Free Language Reachability
Program Verification	Proving uniformity and independence by self-composition and coupling Reasoning about Translation Lookaside Buffers
Proof Assistant	A complete proof of Coq modulo Theory
proof automation	TacticToe: Learning to Reason with HOL4 Tactics
proof search	Deep Proof Search in MELL
proof theory	Deep Proof Search in MELL
propagators	Propagators and Solvers for the Algebra of Modular Systems
Propositional satisfiability	From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes
Q
Quantitative Reasoning	A Quantitative Partial Model-Checking Function and Its Optimisation
query optimization	An Interpolation-based Compiler and Optimizer for Relational Queries (System Implementation Report)
R
reasoner	RACCOON: A Connection Reasoner for the Description Logic ALC
relational logic	Proving uniformity and independence by self-composition and coupling
Relational verification	Synchronizing Constrained Horn Clauses
resolution calculus	First-Order Interpolation and Interpolating Proofs Systems
resource types	Decidable linear list constraints
S
sat	Blocked Clauses in First-Order Logic
SAT solving	Towards a Semantics of Unsatisfiability Proofs with Inprocessing
Semantical Embedding	Theorem Provers For Every Normal Modal Logic
semi-deterministic automata	Seminator: A Tool for Semi-Determinization of Omega-Automata
Semiring	A Quantitative Partial Model-Checking Function and Its Optimisation
separation logic	Bunched Hypersequent Calculi for Distributive Substructural Logics
serious games	Quantified Boolean Formulas: Call the Plumber!
software model checking	Quantified Heap Invariants for Object-Oriented Programs
solvers	Propagators and Solvers for the Algebra of Modular Systems
Soundness	A complete proof of Coq modulo Theory
Stateflow	Automated analysis of Stateflow models
structural rules	Bunched Hypersequent Calculi for Distributive Substructural Logics
superposition	First-Order Interpolation and Interpolating Proofs Systems
symbolic transducer	Translating C# to Branching Symbolic Transducers
system description	Leo-III Version 1.1 (System description)
T
tableau proofs	An Interpolation-based Compiler and Optimizer for Relational Queries (System Implementation Report)
Tableaux	A One-Pass Tree-Shaped Tableau for LTL+Past
term rewriting	Analyzing Runtime Complexity via Innermost Runtime Complexity
Theorem Proving	Deep Network Guided Proof Search Reasoning about Translation Lookaside Buffers
Tractable classes	From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes
Translation Lookaside Buffer	Reasoning about Translation Lookaside Buffers
Type Theory	A complete proof of Coq modulo Theory
U
Unbounded model checking	Synchronizing Constrained Horn Clauses
uniformity	Proving uniformity and independence by self-composition and coupling

Disclaimer | Powered by EasyChair Smart Program