LPAR-22: 22ND INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

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

A
ACTL	Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
Algorithm portfolios	SMTS: Distributed, Visualized Constraint Solving
Amortized Analysis	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
Answer set programming	Symmetry breaking in a new stable model search method
antichain-based tree automata language inclusion
API	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Arithmetic Circuits	Rewriting Environment for Arithmetic Circuit Verification
Automata	Completeness of Left Handed Kleene algebra via Cyclic Proofs Why These Automata Types?
automata learning
Automated reasoning	Loop Analysis by Quantification over Iterations
Axiomatisation	Completeness of Left Handed Kleene algebra via Cyclic Proofs
B
belief revision
bit-width	Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?
Boolean Operations	Why These Automata Types?
Bounded Model Checking	Function Summarization Modulo Theories Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
C
Cardinality Constraints
CEGAR	Towards Smarter MACE-style Model Finders
Clause Learning	Lookahead-Based SMT Solving
Cognitive Reasoning	The Weak Completion Semantics and Equality
Complexity	The Triguarded Fragment of First-order Logic Matching in the Description Logic FL0 with respect to General TBoxes A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
Computational Complexity	On Disallowing Punctual Intervals in Reflexive Semantics of Halpern-Shoham Logic
Computer algebra	Rewriting Environment for Arithmetic Circuit Verification
Constrained Uniform Sampling	Knowledge Compilation meets Uniform Sampling
constraint satisfaction	Linear Tree Constraints
Constraint Solving	Parse Condition: A Symbolic Encoding for LL(1) Parsing
Convex optimization	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Coq	A Verified Theorem Prover Backend Supported by a Monotonic Library
Cost Semantics	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
counterexample	Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
Counterfactual Reasoning	The Weak Completion Semantics and Equality
Craig Interpolation	Function Summarization Modulo Theories
cyclic graphs	Graphs Path Orderings
Cyclic proofs	Completeness of Left Handed Kleene algebra via Cyclic Proofs
D
d-DNNF	Knowledge Compilation meets Uniform Sampling
data mining	Towards Efficient Metaquery Generator
Data streaming
deadlock	Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
Decidability	The Triguarded Fragment of First-order Logic
decision procedures	Two-variable First-Order Logic with Counting in Forests
Default Logic
Deontic Logic
Description Logic	Matching in the Description Logic FL0 with respect to General TBoxes
Description Logics	The Triguarded Fragment of First-order Logic
Digital library	A Verified Theorem Prover Backend Supported by a Monotonic Library
Distributed IC3	SMTS: Distributed, Visualized Constraint Solving
Distributed SMT	SMTS: Distributed, Visualized Constraint Solving
Divide-and-conquer	SMTS: Distributed, Visualized Constraint Solving
E
ECTL	Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
efficient reasoning
epistemic logic	When Are Two Gossips the Same?
EPR	Towards Smarter MACE-style Model Finders
Equational Reasoning	The Weak Completion Semantics and Equality
Erlang	Polymorphic success types for Erlang
Ethical Decision Making	The Weak Completion Semantics and Equality
event lists	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
exclusive-or	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
experimental evaluation	Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?
F
finite model finder	Towards Smarter MACE-style Model Finders
finite satisfiability	Two-variable First-Order Logic with Counting in Forests
First-order logic	Loop Analysis by Quantification over Iterations
Fluent Calculus	The Weak Completion Semantics and Equality
Formal languages and automata theory
Formal verification	Rewriting Environment for Arithmetic Circuit Verification
Fragments of first-order logic	The Triguarded Fragment of First-order Logic
Function Summaries	Function Summarization Modulo Theories
Functor	HoTT-Crypt : A Study in Homotopy Type Theory based on Cryptography
G
Game theory	Alternating Reachability Games with Behavioral and Revenue Objectives
Games	The Involutions-as-Principal Types/Application-as-Unification Analogy
Garbage Collection	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
general satisfiability	Two-variable First-Order Logic with Counting in Forests
Geometry of Interaction	The Involutions-as-Principal Types/Application-as-Unification Analogy
gossip protocols	When Are Two Gossips the Same?
graph games	Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
graph rewriting	Graphs Path Orderings
Groupoid	HoTT-Crypt : A Study in Homotopy Type Theory based on Cryptography
Gödel logics	Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
H
Halpern-Shoham Logic	On Disallowing Punctual Intervals in Reflexive Semantics of Halpern-Shoham Logic
Herbrand expansions	Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
Hierarchical systems	LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
Higher Inductive Type	HoTT-Crypt : A Study in Homotopy Type Theory based on Cryptography
Homotopy Type Theory	HoTT-Crypt : A Study in Homotopy Type Theory based on Cryptography
I
implementations
Incremental Verification	Function Summarization Modulo Theories
Induction	Completeness of Left Handed Kleene algebra via Cyclic Proofs
inductive definitions
Infeasibility analysis	Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
Infinite alphabets	LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
infinite descent
infinite trees	Linear Tree Constraints
inprocessing techniques	A Theory of Satisfiability-Preserving Proofs in SAT Solving
Integer linear programming	LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
interference	A Theory of Satisfiability-Preserving Proofs in SAT Solving
Interior Point Method	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Interpolation	Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
Interval Logic	On Disallowing Punctual Intervals in Reflexive Semantics of Halpern-Shoham Logic
Invariant generation	Loop Analysis by Quantification over Iterations
Isabelle/HOL	A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
K
Kleene algebra	Completeness of Left Handed Kleene algebra via Cyclic Proofs
Knowledge Compilation	Knowledge Compilation meets Uniform Sampling
knowledge-based protocols	When Are Two Gossips the Same?
Kripke Semantics	A Verified Theorem Prover Backend Supported by a Monotonic Library
L
Lambda Calculus	The Involutions-as-Principal Types/Application-as-Unification Analogy
Lamport clocks	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
Lattice Basis Reduction	A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
lazy learning
linear inequalities	Linear Tree Constraints
LL(1) parsing	Parse Condition: A Symbolic Encoding for LL(1) Parsing
logic and computational complexity	Two-variable First-Order Logic with Counting in Forests
Logic Programming	Symmetry breaking in a new stable model search method The Weak Completion Semantics and Equality
Lookahead Heuristic	Lookahead-Based SMT Solving
Loop	Loop Analysis by Quantification over Iterations
LP Solving	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
LTL with arithmetic	LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
Lyndon interpolation	Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
M
Matching	Matching in the Description Logic FL0 with respect to General TBoxes
metaqueries	Towards Efficient Metaquery Generator
Minimal unsatisfiable subsets	Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
Modal Logic	The Triguarded Fragment of First-order Logic
model checking	LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
Model Predictive Control	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Modelling
Monotonicity	A Verified Theorem Prover Backend Supported by a Monotonic Library
multigraphs	Graphs Path Orderings
MUS enumeration	Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
mutable memory	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
N
Nash equilibrium	Alternating Reachability Games with Behavioral and Revenue Objectives
Nonmonotonic Proof Calculus
Numerical Software Verification	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Nuprl	A Verified Theorem Prover Backend Supported by a Monotonic Library
O
Omega-regular languages	Why These Automata Types?
Operational Semantics	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
P
parity games	Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
path orderings	Graphs Path Orderings
Pattern matching
Polymorphism	Polymorphic success types for Erlang
Program analysis	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Program verification	Loop Analysis by Quantification over Iterations
progress measure	Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
Proof checker	A Verified Theorem Prover Backend Supported by a Monotonic Library
Propositional Satisfiability
protocol verification	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
pushdown automata	Linear Tree Constraints
Q
quantified bit-vectors	Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?
R
Random walks and Markov chains
rational synthesis	Alternating Reachability Games with Behavioral and Revenue Objectives
Reachability games	Alternating Reachability Games with Behavioral and Revenue Objectives
read-over-write simplification	Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Regular languages	Linear Tree Constraints Completeness of Left Handed Kleene algebra via Cyclic Proofs
relational database	Towards Efficient Metaquery Generator
resource analysis	Linear Tree Constraints
Resource Bound Analysis	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
Reversible Computations	The Involutions-as-Principal Types/Application-as-Unification Analogy
rewrite orderings	Graphs Path Orderings
S
SAT	Towards Smarter MACE-style Model Finders Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
SAT solving	A Theory of Satisfiability-Preserving Proofs in SAT Solving Knowledge Compilation meets Uniform Sampling
Satisfiability Modulo Theories	Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? Function Summarization Modulo Theories
satisfiability modulo theory	Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Skolemization	Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic
SMT encoding	Parse Condition: A Symbolic Encoding for LL(1) Parsing
SMT Solving	Lookahead-Based SMT Solving
Software Verification	Function Summarization Modulo Theories
Stable models	Symmetry breaking in a new stable model search method
Static Analysis	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
Sub-propositional Fragments	On Disallowing Punctual Intervals in Reflexive Semantics of Halpern-Shoham Logic
Success Types	Polymorphic success types for Erlang
Succinctness	Why These Automata Types?
symbolic computation	Quasipolynomial Set-Based Symbolic Algorithms for Parity Games
Symmetry breaking	Symmetry breaking in a new stable model search method
T
Tableaux System
termination	Loop Analysis by Quantification over Iterations Graphs Path Orderings
The guarded fragment	The Triguarded Fragment of First-order Logic
The two-variable fragment	The Triguarded Fragment of First-order Logic
theory of arrays	Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
Three-Valued Lukasiewicz Logic	The Weak Completion Semantics and Equality
Tree Automata	Matching in the Description Logic FL0 with respect to General TBoxes
two-variable logic with counting quantifiers	Two-variable First-Order Logic with Counting in Forests
Type Inference	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
Type Systems	Automatic Space Bound Analysis for Functional Programs with Garbage Collection
Types	Polymorphic success types for Erlang
U
Univalence	HoTT-Crypt : A Study in Homotopy Type Theory based on Cryptography
unranked trees/forests	Two-variable First-Order Logic with Counting in Forests
Unsatisfiability analysis	Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
V
verification
Verified theorem prover backend	A Verified Theorem Prover Backend Supported by a Monotonic Library
W
Weak Completion	The Weak Completion Semantics and Equality
web-based GUI	SMTS: Distributed, Visualized Constraint Solving
witness	Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse
word combinatorics	Linear Tree Constraints
Y
YubiHSM	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
YubiKey	Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA

Disclaimer | Powered by EasyChair Smart Program