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

Disclaimer | Powered by EasyChair Smart Program