LPAR-20: 20TH INTERNATIONAL CONFERENCES ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

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

A
Abstract Interpretation	Gamifying Program Analysis Abstract Domains and Solvers for Sets Reasoning Boolean Formulas for the Static Identification of Injection Attacks in Java
Abstraction	Automated Discovery of Simulation Between Programs
Answer Set Program	Reasoning in the presence of inconsistency through Preferential ALC
answer set programming	Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
attacks	Analyzing Internet Routing Security Using Model Checking
automata characterization	Controller synthesis for MDPs and Frequency LTL\GU
automated benchmarking	Automated Benchmarking of Incremental SAT and QBF Solvers
Automated Deduction	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
automated reasoning	Sharing HOL4 and HOL Light proof knowledge
automated testing	Automated Benchmarking of Incremental SAT and QBF Solvers
automated theorem proving	FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover Reasoning About Loops Using Vampire in KeY
automatic theorem proving	TIP: Tools for Inductive Provers
automaton	Decidability, Introduction Rules and Automata
automaton minimization	SAT-based Minimization of Deterministic ω-Automata
automaton synthesis	SAT-based Minimization of Deterministic ω-Automata
axiomatization	Reasoning about embedded dependencies using inclusion dependencies
B
B Method	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
Belief Change	On Anti-Subsumptive Knowledge Enforcement
beta-nomalization	There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners
BGP	Analyzing Internet Routing Security Using Model Checking
bigraphs	An adequate compositional encoding of bigraph structure in linear logic with subexponentials
binary decision diagrams	Boolean Formulas for the Static Identification of Injection Attacks in Java
bit-blasting	Fine grained SMT proofs for the theory of fixed-width bit-vectors
bit-vectors	Fine grained SMT proofs for the theory of fixed-width bit-vectors
blocked clause elimination	Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
Boolean Circuits	A New Proof of P-time Completeness of Linear Lambda Calculus
boolean functions	Boolean Formulas for the Static Identification of Injection Attacks in Java
Boolean Logic	On Anti-Subsumptive Knowledge Enforcement
C
causality and responsibility	Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
chase	Reasoning about embedded dependencies using inclusion dependencies
Choose operator	Compiling Hilbert's epsilon operator
Classical logic	A Lightweight Double-negation Translation
clause learning	Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
combining knowledge	Sharing HOL4 and HOL Light proof knowledge
Communication Primitive	On the expressive power of communication primitives in parameterised systems
Compilation	Compiling Hilbert's epsilon operator
Completeness Theorem	Normalization by Completeness with Heyting Algebras
computational ethics	Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
concurrent programs	Verification of Concurrent Programs Using Trace Abstraction Refinement
conflict analysis	On Conflicts and Strategies in QBF
connection tableau	FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
Constraint Solving	Abstract Domains and Solvers for Sets Reasoning
Constructive logic	A Lightweight Double-negation Translation
controller synthesis	Controller synthesis for MDPs and Frequency LTL\GU
CPS hierarchy	On Subexponentials, Synthetic Connectives, and Multi-Level Delimited Control
Crowd sourcing	Gamifying Program Analysis
cryptography	Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
cube learning	Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
cut-elimination	Decidability, Introduction Rules and Automata
D
data structures	There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners
De Bruijn's levels	A Fast Interpreter for λProlog
decidablity	Decidability, Introduction Rules and Automata
Deduction Modulo	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
Deductive games	Cobra: A Tool for Solving General Deductive Games
Dedukti	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
delimited control operators	On Subexponentials, Synthetic Connectives, and Multi-Level Delimited Control
dependence logic	Reasoning about embedded dependencies using inclusion dependencies
Description Logic	Reasoning in the presence of inconsistency through Preferential ALC
Description Logics	Tableau-based Revision over SHIQ TBoxes
deterministic ω-automata	SAT-based Minimization of Deterministic ω-Automata
doctrine of double effect	Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
Double-negation translation	A Lightweight Double-negation Translation
Dynamic Epistemic Logic	A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic
dynamic/hybrid monitors	Value Sensitivity and Observable Abstract Values for Information Flow Control
E
embedded dependency	Reasoning about embedded dependencies using inclusion dependencies
Encoding for SMT solver	Compiling Hilbert's epsilon operator
equality generating dependency	Reasoning about embedded dependencies using inclusion dependencies
explicit context	A Contextual Logical Framework
Expressive Power	On the expressive power of communication primitives in parameterised systems
F
first-order logic	A Lightweight Double-negation Translation Reasoning About Loops Using Vampire in KeY
First-order logics	Skolemization for Substructural Logics
Focused proof systems	Focused labeled proof systems for modal logic
Focusing	Proof Search in Nested Sequent Calculi
frequency LTL	Controller synthesis for MDPs and Frequency LTL\GU
G
Geometric formulas	Focused labeled proof systems for modal logic
Graded Temporal Logic	On CTL* with Graded Path Modalities
H
hard-combinatorial problems	Compositional Propositional Proofs
higher-order logic	Sharing HOL4 and HOL Light proof knowledge There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners
Hilbert's epsilon operator	Compiling Hilbert's epsilon operator
Horn clause	Finding Inconsistencies in Programs with Loops
Horn clauses	Automated Discovery of Simulation Between Programs
I
implication problem	Reasoning about embedded dependencies using inclusion dependencies
implicit complexity	Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
inclusion dependency	Reasoning about embedded dependencies using inclusion dependencies
Inconsistency tolerant	Reasoning in the presence of inconsistency through Preferential ALC
Inconsistent code	Finding Inconsistencies in Programs with Loops
incremental solving	Automated Benchmarking of Incremental SAT and QBF Solvers
induction	TIP: Tools for Inductive Provers
Inductive synthesis	Automated Discovery of Simulation Between Programs
information flow	Boolean Formulas for the Static Identification of Injection Attacks in Java
Information leakage	Cobra: A Tool for Solving General Deductive Games
information-flow control	Value Sensitivity and Observable Abstract Values for Information Flow Control
internal proof guidance	FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
Internet	Analyzing Internet Routing Security Using Model Checking
interpreter	A Fast Interpreter for λProlog
Intuitionistic Logic	SAT modulo intuitionistic implications Normalization by Completeness with Heyting Algebras
intuitionistic modal logic	A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic
L
Labeled proof systems	Focused labeled proof systems for modal logic
Labelled Sequent Calculus	A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic
Labelled systems	Proof Search in Nested Sequent Calculi
lambda-calculus	Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
lambdaprolog	A Fast Interpreter for λProlog
leancop	FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
LFSC	Fine grained SMT proofs for the theory of fixed-width bit-vectors
linear dependent types	Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
Linear Lambda Calculus	A New Proof of P-time Completeness of Linear Lambda Calculus
linear logic	A Contextual Logical Framework A New Proof of P-time Completeness of Linear Lambda Calculus On Subexponentials, Synthetic Connectives, and Multi-Level Delimited Control An adequate compositional encoding of bigraph structure in linear logic with subexponentials
linear types	Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
Logic programming	Modular Multiset Rewriting
logical constraints	ConsTrained Rewriting tooL
logical framework	A Contextual Logical Framework
Logics	Automated Theorem Proving by Translation to Description Logic
loop invariant	Reasoning About Loops Using Vampire in KeY
M
machine learning	Gamifying Program Analysis Sharing HOL4 and HOL Light proof knowledge FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
MDP	Controller synthesis for MDPs and Frequency LTL\GU
Modal logic	Focused labeled proof systems for modal logic
Modal logics	Proof Search in Nested Sequent Calculi
Model Checking	On the expressive power of communication primitives in parameterised systems
model finding	SAT modulo intuitionistic implications
model-checking	Analyzing Internet Routing Security Using Model Checking Verification of Concurrent Programs Using Trace Abstraction Refinement
Modularity	Modular Multiset Rewriting
monomorphisation	TIP: Tools for Inductive Provers
moral reasoning	Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
MSO	Symbolic WS1S
Multiset Rewriting	Modular Multiset Rewriting
N
Natural Deduction	Normalization by Completeness with Heyting Algebras
Nested sequents	Proof Search in Nested Sequent Calculi
non-monotonic reasoning	Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
Normalization by Evaluation	Normalization by Completeness with Heyting Algebras
O
Ontology	Tableau-based Revision over SHIQ TBoxes
opinion	Application of Trace-Based Subjective Logic to User Preferences Modeling
P
P-time Completeness	A New Proof of P-time Completeness of Linear Lambda Calculus
parallel SAT solving	Compositional Propositional Proofs
Parameterised Systems	On the expressive power of communication primitives in parameterised systems
partial correctness	Reasoning About Loops Using Vampire in KeY
partial order	Verification of Concurrent Programs Using Trace Abstraction Refinement
Partial-Max-SAT	On Anti-Subsumptive Knowledge Enforcement
Path Quantifiers	On CTL* with Graded Path Modalities
Preemption	On Anti-Subsumptive Knowledge Enforcement
preprocessing	Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
Probabilistic coupling	Relational reasoning via probabilistic coupling
program analysis	Using Program Synthesis for Program Analysis
program synthesis	Using Program Synthesis for Program Analysis
program verification	ConsTrained Rewriting tooL
proof advice	Sharing HOL4 and HOL Light proof knowledge
proof checking	Compositional Propositional Proofs
proof libraries	Sharing HOL4 and HOL Light proof knowledge
Proof search	Proof Search in Nested Sequent Calculi
proofs	Fine grained SMT proofs for the theory of fixed-width bit-vectors
Public Announcement Logic	A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic
Pushdown systems	Synchronized Recursive Timed Automata Decidability, Introduction Rules and Automata
Q
QBF	Playing with Quantified Satisfaction Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination Automated Benchmarking of Incremental SAT and QBF Solvers On Conflicts and Strategies in QBF
quantification	On Conflicts and Strategies in QBF
quantified Boolean formulas	Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
Quantifier elimination	Playing with Quantified Satisfaction Automated Discovery of Simulation Between Programs
quantitative logics	Controller synthesis for MDPs and Frequency LTL\GU
R
Reachability problem	Synchronized Recursive Timed Automata
reductions	Analyzing Internet Routing Security Using Model Checking
Relational property	Relational reasoning via probabilistic coupling
resolution	Fine grained SMT proofs for the theory of fixed-width bit-vectors
Revision	Tableau-based Revision over SHIQ TBoxes
routing	Analyzing Internet Routing Security Using Model Checking
Russell's definite description operator	Compiling Hilbert's epsilon operator
S
SAT	SAT-based Minimization of Deterministic ω-Automata Fine grained SMT proofs for the theory of fixed-width bit-vectors SAT modulo intuitionistic implications Automated Benchmarking of Incremental SAT and QBF Solvers
Satisfiability	On CTL* with Graded Path Modalities
search-based solving	Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
second-order logic	Using Program Synthesis for Program Analysis
security	Analyzing Internet Routing Security Using Model Checking
sequent calculus	Decidability, Introduction Rules and Automata
Set Theory	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
Sets	Abstract Domains and Solvers for Sets Reasoning
Simulation relation	Automated Discovery of Simulation Between Programs
Skolemization	Skolemization for Substructural Logics
SMT	Symbolic WS1S Playing with Quantified Satisfaction Fine grained SMT proofs for the theory of fixed-width bit-vectors SAT modulo intuitionistic implications Finding Inconsistencies in Programs with Loops
Specification mining	Gamifying Program Analysis
stable model semantics	Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
static analysis	Boolean Formulas for the Static Identification of Injection Attacks in Java
static verification	Reasoning About Loops Using Vampire in KeY
strategies	On Conflicts and Strategies in QBF
Strategy synthesis	Cobra: A Tool for Solving General Deductive Games
subexponentials	On Subexponentials, Synthetic Connectives, and Multi-Level Delimited Control An adequate compositional encoding of bigraph structure in linear logic with subexponentials
Subjective Logic	Application of Trace-Based Subjective Logic to User Preferences Modeling
Substructural logics	Skolemization for Substructural Logics
Subsumption	On Anti-Subsumptive Knowledge Enforcement
symbolic automata	Symbolic WS1S
T
Tableau	Reasoning in the presence of inconsistency through Preferential ALC
Tableau algorithm	Tableau-based Revision over SHIQ TBoxes
term rewriting	ConsTrained Rewriting tooL
theorem proving	SAT modulo intuitionistic implications There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners Automated Theorem Proving by Translation to Description Logic
Timed automata	Synchronized Recursive Timed Automata
tool	SAT-based Minimization of Deterministic ω-Automata
traces	Application of Trace-Based Subjective Logic to User Preferences Modeling
Translation	Automated Theorem Proving by Translation to Description Logic
tuple generating dependency	Reasoning about embedded dependencies using inclusion dependencies
type systems	Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
Typed Proof Search	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
U
user preferences	Application of Trace-Based Subjective Logic to User Preferences Modeling
V
value-sensitivity	Value Sensitivity and Observable Abstract Values for Information Flow Control
variable expansion	Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
Verification	Abstract Domains and Solvers for Sets Reasoning Relational reasoning via probabilistic coupling Verification of Concurrent Programs Using Trace Abstraction Refinement
Verification-aware programming language	Compiling Hilbert's epsilon operator
Z
Zenon Modulo	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo

Disclaimer | Powered by EasyChair Smart Program