LPAR 2023: 24TH INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

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

A
abduction	An Interactive SMT Tactic in Coq using Abductive Reasoning
Abstraction Refinement
algebraic data types	Collaborative Inference of Combined Invariants
Answer Set Programming	A Fast and Accurate ASP Counting Based Network Reliability Estimator
arithmetic	Refining Unification with Abstraction A Mathematical Benchmark for Inductive Theorem Provers
Automata-based	Model Checking Omega-Regular Hyperproperties with AutoHyperQ
Automated reasoning	Embedding Intuitionistic into Classical Logic On the Complexity of Convex and Reverse Convex Prequadratic Constraints
automated theorem provers	A Mathematical Benchmark for Inductive Theorem Provers
automated theorem proving	Refining Unification with Abstraction How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
B
benchmark	A Mathematical Benchmark for Inductive Theorem Provers
Blockchain	HoRStify: Sound Security Analysis of Smart Contracts
C
causality	Counterfactuals Modulo Temporal Logics
CEGAR	Collaborative Inference of Combined Invariants
certified implementation	Keep me out of the loop: a more flexible choreographic projection
choreographic programming	Keep me out of the loop: a more flexible choreographic projection
Clause Evaluation	Guiding an Instantiation Prover with Graph Neural Networks
clause selection	How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
collaborative inference	Collaborative Inference of Combined Invariants
Computational complexity	On the Complexity of Convex and Reverse Convex Prequadratic Constraints
computer-aided mathematics	Computer-aided Mathematics: Successes, Advances, and Trust
conditioning	On the computation of conditioning in weighted belief bases
Conflict Analysis	Analyzing Multiple Conflicts in SAT: An Experimental Evaluation
constrained Horn clauses	Collaborative Inference of Combined Invariants
Constraints	Scalable Probabilistic Routes
Continuous Double Auctions	Efficient and Verified Continuous Double Auctions
contract-based reasoning	Trace-based Deductive Verification
Coq	An Interactive SMT Tactic in Coq using Abductive Reasoning
Countable Graphs	Mechanising Hall’s Theorem for Countable Graphs
counterfactuals	Counterfactuals Modulo Temporal Logics
cvc5	An Interactive SMT Tactic in Coq using Abductive Reasoning
D
decidability	Counterfactuals Modulo Temporal Logics
Decision Diagrams	Scalable Probabilistic Routes
Declarative Programming	Software Formal Verification by Rewriting Logic and Declarative Programming
Declarative Semantics	LDL: the Logic of Differentiable Logics
deductive verification	Trace-based Deductive Verification
Dependency Analysis	HoRStify: Sound Security Analysis of Smart Contracts
Differentiable Logic	LDL: the Logic of Differentiable Logics
distributed protocols	Keep me out of the loop: a more flexible choreographic projection
E
Ethereum	HoRStify: Sound Security Analysis of Smart Contracts
Experimental Evaluation	Analyzing Multiple Conflicts in SAT: An Experimental Evaluation
F
Financial Markets	Efficient and Verified Continuous Double Auctions
finite fields	SMT Solving over Finite Field Arithmetic
finite satisfiability problem	An excursion to the border of decidability: between two- and three-variable logic
first-order model building	Exploring Partial Models with SCL
first-order reasoning	Exploring Partial Models with SCL
Formal Specification and Verification	Efficient and Verified Continuous Double Auctions
formal verification	Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Fuzzy Logic	LDL: the Logic of Differentiable Logics
G
graph neural network	How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
Graph Neural Networks	Guiding an Instantiation Prover with Graph Neural Networks
H
Hall's Theorem	Mechanising Hall’s Theorem for Countable Graphs
hypercubes	Toward Optimal Radio Colorings of Hypercubes via SAT-solving
hyperproperties	Model Checking Omega-Regular Hyperproperties with AutoHyperQ Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
HyperQPTL	Model Checking Omega-Regular Hyperproperties with AutoHyperQ
I
induction	A Mathematical Benchmark for Inductive Theorem Provers
inductive invariants	Collaborative Inference of Combined Invariants
inductive theorem provers	A Mathematical Benchmark for Inductive Theorem Provers
infinite model	Experiments on Infinite Model Finding in SMT Solving
Interactive Theorem Proving	Mechanising Hall’s Theorem for Countable Graphs
Interpretations	Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
Intuitionistic Logic	Embedding Intuitionistic into Classical Logic
Isabelle/HOL	Mechanising Hall’s Theorem for Countable Graphs
K
k-safety	Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
Knowledge Compilation	Scalable Probabilistic Routes
L
language-parametric	Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
linear integer arithmetic	Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
logic	Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
M
Machine Learning	Guiding an Instantiation Prover with Graph Neural Networks LDL: the Logic of Differentiable Logics How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
modal logic	Counterfactuals Modulo Temporal Logics
Model Checking	Model Checking Omega-Regular Hyperproperties with AutoHyperQ
Model Theory	Embedding Intuitionistic into Classical Logic
mu-calculus	Trace-based Deductive Verification
N
Network Reliability	A Fast and Accurate ASP Counting Based Network Reliability Estimator
Neural Networks
Non-linear arithmetic	On the Complexity of Convex and Reverse Convex Prequadratic Constraints
non-linear integer arithmetic	Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
non-linear real arithmetic	Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
non-redundant learning	Exploring Partial Models with SCL
O
OEIS	A Mathematical Benchmark for Inductive Theorem Provers
P
parallel computing	Computer-aided Mathematics: Successes, Advances, and Trust
polynomial arithmetic	SMT Solving over Finite Field Arithmetic
possibility theory	On the computation of conditioning in weighted belief bases
Probabilistic Logic	LDL: the Logic of Differentiable Logics
Program Analysis	HoRStify: Sound Security Analysis of Smart Contracts
Promptness	Model Checking Omega-Regular Hyperproperties with AutoHyperQ
Proof Theory	Embedding Intuitionistic into Classical Logic
proofs	Computer-aided Mathematics: Successes, Advances, and Trust
Q
QPTL	Model Checking Omega-Regular Hyperproperties with AutoHyperQ
R
radio colorings	Toward Optimal Radio Colorings of Hypercubes via SAT-solving
Red-Black Trees	Efficient and Verified Continuous Double Auctions
Rewriting Lopic	Software Formal Verification by Rewriting Logic and Declarative Programming
Routing	Scalable Probabilistic Routes
S
Sampling	Scalable Probabilistic Routes
SAT	Analyzing Multiple Conflicts in SAT: An Experimental Evaluation Toward Optimal Radio Colorings of Hypercubes via SAT-solving
SAT solving	Computer-aided Mathematics: Successes, Advances, and Trust
Satisfiability modulo theories	On the Complexity of Convex and Reverse Convex Prequadratic Constraints
satisfiability problem	An excursion to the border of decidability: between two- and three-variable logic
saturation-based theorem proving	How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
SCL	Exploring Partial Models with SCL
Security	HoRStify: Sound Security Analysis of Smart Contracts
Smart Contract	HoRStify: Sound Security Analysis of Smart Contracts
smart contracts	Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
SMT	Experiments on Infinite Model Finding in SMT Solving
SMT solving	Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification SMT Solving over Finite Field Arithmetic
SMTCoq	An Interactive SMT Tactic in Coq using Abductive Reasoning
SYGUS	Experiments on Infinite Model Finding in SMT Solving
symbolic execution	Trace-based Deductive Verification
T
temporal logic	Counterfactuals Modulo Temporal Logics
Theorem Proving	Guiding an Instantiation Prover with Graph Neural Networks Keep me out of the loop: a more flexible choreographic projection
three-variable logic	An excursion to the border of decidability: between two- and three-variable logic
Tool	HoRStify: Sound Security Analysis of Smart Contracts
TPTP	Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
trace contracts	Trace-based Deductive Verification
triangular sets	SMT Solving over Finite Field Arithmetic
two-variable logic	An excursion to the border of decidability: between two- and three-variable logic
Types	LDL: the Logic of Differentiable Logics
U
Unification	Refining Unification with Abstraction
Unification with Abstraction	Refining Unification with Abstraction
uniform one-dimensional fragment	An excursion to the border of decidability: between two- and three-variable logic
V
Verification	Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic Computer-aided Mathematics: Successes, Advances, and Trust Software Formal Verification by Rewriting Logic and Declarative Programming
W
weighted knowledge bases	On the computation of conditioning in weighted belief bases
Weighted Model Counting	A Fast and Accurate ASP Counting Based Network Reliability Estimator

Disclaimer | Powered by EasyChair Smart Program