Talk Keyword Index

TALK KEYWORD INDEX

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

Shortcuts: A B C D E F G H I K L M N O P Q R S T V W

A
Abstract Interpretation	Automatic Detection of Vulnerable Variables for CTL Properties of Programs
action model	Symbolic Realisation of Epistemic Processes
Admissibility	A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
Andrews-Curtis conjecture	Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II
Arithmetic	VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic On the Idea of Exploration-guided Satisfiability Checking
Arrays	On SMT Theory Design: The Case of Sequences
automated inductive reasoning	Sorting without Sorts
automated reasoning	First Experiments with Neural CVC5 Scaling CheckMate for Game-Theoretic Security Sorting without Sorts Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II Automated Reasoning with Tangles: towards Quantum Verification Applications
automated software verification	Sorting without Sorts
Automated Theorem Proving	Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery A Generic Deskolemization Strategy Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper) Sorting without Sorts Automated Theorem Provers Help Improve Large Language Model Reasoning Automated Theorem Proving for Prolog Verification
B
bags	Verifying SQL queries using theories of tables and relations - virtual talk over Zoom
base conversion	Numeric Base Conversion with Rewriting
belief change	A Tool for Reasoning about Trust and Belief
blockchain protocols	Scaling CheckMate for Game-Theoretic Security
Blocked-clause Addition	Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
Bounded-Tree Width	Tree-Verifiable Graph Grammars
btor2mlir	Efficient Simulation for Hardware Model Checking
Bubble sort	Certification of Tail Recursive Bubble--Sort in Theorema and Coq
Business	Internships in Mauritius
BV	Deep Inference in Proof Search: The Need for Shallow Inference
C
call-by-name	Hybrid Intersection Types for PCF
call-by-value	Hybrid Intersection Types for PCF
certification	Certifying Incremental SAT Solving Translating HOL-Light proofs to Coq Certification of Tail Recursive Bubble--Sort in Theorema and Coq
CHC Solving	Golem: A Flexibile and Efficient Solver for Constrained Horn Clauses
choice	Experiments with Choice in Dependently-Typed Higher-Order Logic
CNF formulas	Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
combinatorial group theory	Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II
Commerce	Internships in Mauritius
concept alignment	Translating HOL-Light proofs to Coq
confluence	Confluence for Proof-Nets via Parallel Cut Elimination
Constrained Horn Clauses	Automatic Bit- and Memory-Precise Verification of eBPF Code Golem: A Flexibile and Efficient Solver for Constrained Horn Clauses Automated Test Case Generation for Solidity Using Constrained Horn Clauses
constraint solving	Minimizing Sorting Networks at the Sub-Comparator Level
Coq	Certification of Tail Recursive Bubble--Sort in Theorema and Coq
CTL	Automatic Detection of Vulnerable Variables for CTL Properties of Programs
cut-elimination	Confluence for Proof-Nets via Parallel Cut Elimination
Cylindric Algebraic Decomposition	On the Idea of Exploration-guided Satisfiability Checking
D
datalog	Fuzzy Datalog$^\exists$ over Arbitrary t-norms
decision lists	Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
Decision Procedure	VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
deep inference	Deep Inference in Proof Search: The Need for Shallow Inference
dependent HOL	Experiments with Choice in Dependently-Typed Higher-Order Logic
dependent type theory	Translating HOL-Light proofs to Coq
Description logics	A Case for Extensional Non-Wellfounded Metamodeling
E
eBPF	Automatic Bit- and Memory-Precise Verification of eBPF Code
epistemic logic	Symbolic Realisation of Epistemic Processes
epistemic process	Symbolic Realisation of Epistemic Processes
epsilon calculus	On Translations of Epsilon Proofs to LK
Evaluation	30 Years of Faster and Faster SAT Solving
evaluation strategies	Hybrid Intersection Types for PCF
F
Facilitator	Internships in Mauritius
First Order Logic	Automated Theorem Provers Help Improve Large Language Model Reasoning
first-order theorem proving	Sorting without Sorts
formal methods	Sorting without Sorts
Free-Variable Tableaux	A Generic Deskolemization Strategy
fusion	On Symbolic Derivatives and Transition Regexes
fuzzy logic	Fuzzy Datalog$^\exists$ over Arbitrary t-norms
G
game semantics	A Simple Token Game and its Logic
game-theoretic security	Scaling CheckMate for Game-Theoretic Security
Games semantics	Reasoning About Group Polarization: From Semantic Games to Sequent Systems
Graph Grammars	Tree-Verifiable Graph Grammars
guarded commands	Alternate Semantics of the Guarded Conditional
H
Herbrand sequents	Herbrand's Theorem in Inductive Proofs
higher-order logic	Translating HOL-Light proofs to Coq
Hilbert's epsilon formalism	On Translations of Epsilon Proofs to LK
hypergraphs	Confluence for Proof-Nets via Parallel Cut Elimination
I
incentive compatibility	Scaling CheckMate for Game-Theoretic Security
Incremental SAT	Certifying Incremental SAT Solving
Induction	Rewriting and Inductive Reasoning
inductive proofs	Herbrand's Theorem in Inductive Proofs On Proof Schemata and Primitive Recursive Arithmetic
Inferentialism	A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
Internships	Internships in Mauritius
intersection types	Hybrid Intersection Types for PCF
Intuitionistic Logic	A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
involutory quandles	Automated Reasoning with Tangles: towards Quantum Verification Applications
K
Knowledge representation	A Tool for Reasoning about Trust and Belief A Case for Extensional Non-Wellfounded Metamodeling
L
lambda calculus	Hybrid Intersection Types for PCF
Large Language Models	Automated Theorem Provers Help Improve Large Language Model Reasoning
linear logic	Confluence for Proof-Nets via Parallel Cut Elimination A Simple Token Game and its Logic
LIRA	VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
Logic	On SMT Theory Design: The Case of Sequences A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
Logic Programming	Automated Theorem Provers Help Improve Large Language Model Reasoning Automated Theorem Proving for Prolog Verification
logical frameworks	Translating HOL-Light proofs to Coq
lookahead	On Symbolic Derivatives and Transition Regexes
M
Machine learning	First Experiments with Neural CVC5
Mauritius	Internships in Mauritius
MCSAT	On the Idea of Exploration-guided Satisfiability Checking
Metamodeling	A Case for Extensional Non-Wellfounded Metamodeling
MLL	Deep Inference in Proof Search: The Need for Shallow Inference
Modal logic	Reasoning About Group Polarization: From Semantic Games to Sequent Systems
model checking	Efficient Simulation for Hardware Model Checking
Model Counting	Automated Synthesis: An Ideal Meeting Ground for Symbolic Reasoning and Machine Learning
Monadic Second Order Logic	Tree-Verifiable Graph Grammars
N
Natural Language	Automated Theorem Provers Help Improve Large Language Model Reasoning
Natural Style Proving	A Natural Style Prover in Theorema Using Sequent Calculus with Unit Propagation
non-linear integer arithmetic	Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
nondeterminism	Deep Inference in Proof Search: The Need for Shallow Inference Alternate Semantics of the Guarded Conditional
NP-hardness	Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
numeric bases	Numeric Base Conversion with Rewriting
O
Ontologies	A Case for Extensional Non-Wellfounded Metamodeling
operational semantics	Alternate Semantics of the Guarded Conditional
P
parallel reduction	Confluence for Proof-Nets via Parallel Cut Elimination
Partial correctness	Automated Theorem Proving for Prolog Verification
Portfolio of Strategies	Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper)
Preprocessing	Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
primitive recursive arithmetic	On Proof Schemata and Primitive Recursive Arithmetic
Probabilistic Programs	Probabilistic Programs. Verified. Push-Button.
program optimization	Minimizing Sorting Networks at the Sub-Comparator Level
Program Verification	Automatic Bit- and Memory-Precise Verification of eBPF Code Automatic Detection of Vulnerable Variables for CTL Properties of Programs Probabilistic Programs. Verified. Push-Button.
Prolog	Automated Theorem Proving for Prolog Verification
Proof Certificate	A Generic Deskolemization Strategy
proof checking	Certifying Incremental SAT Solving
Proof schema	Herbrand's Theorem in Inductive Proofs On Proof Schemata and Primitive Recursive Arithmetic
proof search	Deep Inference in Proof Search: The Need for Shallow Inference
proof theory	A Simple Token Game and its Logic A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
proof transformation	Translating HOL-Light proofs to Coq
proof translation	Experiments with Choice in Dependently-Typed Higher-Order Logic Translating HOL-Light proofs to Coq
proof-net	Confluence for Proof-Nets via Parallel Cut Elimination
Proof-Search Procedures	A Generic Deskolemization Strategy
Proof-theoretic Semantics	A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
Proofs	Certifying Incremental SAT Solving
propositional dynamic logic	Symbolic Realisation of Epistemic Processes
Propositional Logic	A Natural Style Prover in Theorema Using Sequent Calculus with Unit Propagation
protocol verification	Scaling CheckMate for Game-Theoretic Security
Q
Quantifier Elimination	VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
quantitative models	Hybrid Intersection Types for PCF
quantum verification	Automated Reasoning with Tangles: towards Quantum Verification Applications
R
Reasoning	Automated Theorem Provers Help Improve Large Language Model Reasoning
recursive programs	Sorting without Sorts
relations	Verifying SQL queries using theories of tables and relations - virtual talk over Zoom
Resolution calculus	Herbrand's Theorem in Inductive Proofs
resource logic	A Simple Token Game and its Logic
Reuse	Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper)
Rewriting	Rewriting and Inductive Reasoning Translating HOL-Light proofs to Coq
S
SAT	30 Years of Faster and Faster SAT Solving Automated Synthesis: An Ideal Meeting Ground for Symbolic Reasoning and Machine Learning
SAT-solving	Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
satisfiability	Minimizing Sorting Networks at the Sub-Comparator Level
Satisfiability Modulo Theories	Combining Combination Properties: Minimal Models On SMT Theory Design: The Case of Sequences
Saturation	Rewriting and Inductive Reasoning
Saturation-based proving	Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper)
Security	Automatic Detection of Vulnerable Variables for CTL Properties of Programs
Sequences	On SMT Theory Design: The Case of Sequences
Sequent Calculus	On Translations of Epsilon Proofs to LK A Natural Style Prover in Theorema Using Sequent Calculus with Unit Propagation
Sequent system	Reasoning About Group Polarization: From Semantic Games to Sequent Systems
Set theory	A Case for Extensional Non-Wellfounded Metamodeling
sets	Verifying SQL queries using theories of tables and relations - virtual talk over Zoom
simulation	Efficient Simulation for Hardware Model Checking
Skolemization	A Generic Deskolemization Strategy
SMT	Verifying SQL queries using theories of tables and relations - virtual talk over Zoom VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic On Symbolic Derivatives and Transition Regexes On the Idea of Exploration-guided Satisfiability Checking Automated Synthesis: An Ideal Meeting Ground for Symbolic Reasoning and Machine Learning
Solidity	Automated Test Case Generation for Solidity Using Constrained Horn Clauses
Solve business problems	Internships in Mauritius
sorting	Certification of Tail Recursive Bubble--Sort in Theorema and Coq
sorting algorithms	Sorting without Sorts
sorting networks	Minimizing Sorting Networks at the Sub-Comparator Level
SQL	Verifying SQL queries using theories of tables and relations - virtual talk over Zoom
Static analysis	Automated Synthesis of Decision Lists for Polynomial Specifications over Integers Automatic Detection of Vulnerable Variables for CTL Properties of Programs
Steamroller Problems	Automated Theorem Provers Help Improve Large Language Model Reasoning
Strategy Invention	Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery
Strategy Scheduling	Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery
Superposition	Rewriting and Inductive Reasoning
superposition calculus	Sorting without Sorts
symbolic abstraction	Symbolic Realisation of Epistemic Processes
symbolic automaton	On Symbolic Derivatives and Transition Regexes
Symbolic Enumeration	Automated Test Case Generation for Solidity Using Constrained Horn Clauses
symbolic execution	Symbolic Realisation of Epistemic Processes
Symbolic Model Checking	Probabilistic Programs. Verified. Push-Button.
synthesis	Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
system description	A Tool for Reasoning about Trust and Belief
T
tables	Verifying SQL queries using theories of tables and relations - virtual talk over Zoom
tangles	Automated Reasoning with Tangles: towards Quantum Verification Applications
TBA1	TBA TBA TBA TBA
TBA2	TBA TBA TBA TBA
TBA3	TBA TBA TBA TBA
temporal logic	On Symbolic Derivatives and Transition Regexes
term rewriting	Numeric Base Conversion with Rewriting
Termination	Automated Theorem Proving for Prolog Verification
Test coverage	Automated Test Case Generation for Solidity Using Constrained Horn Clauses
Testcase Generation	Automated Test Case Generation for Solidity Using Constrained Horn Clauses
Theorem proving	First Experiments with Neural CVC5 30 Years of Faster and Faster SAT Solving
Theorema	A Natural Style Prover in Theorema Using Sequent Calculus with Unit Propagation Certification of Tail Recursive Bubble--Sort in Theorema and Coq
Theory combination	Combining Combination Properties: Minimal Models
Theory politeness	Combining Combination Properties: Minimal Models
Transition System	Golem: A Flexibile and Efficient Solver for Constrained Horn Clauses
trust	A Tool for Reasoning about Trust and Belief
tuple-generating dependencies	Fuzzy Datalog$^\exists$ over Arbitrary t-norms
V
verification	Efficient Simulation for Hardware Model Checking Automated Theorem Proving for Prolog Verification
Virtual Substitution	VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
W
weakest liberal precondition	Symbolic Realisation of Epistemic Processes
Weakest Preconditions	Probabilistic Programs. Verified. Push-Button.