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
Artificial Intelligence	The Application of Artificial Intelligence in the Financial Services Sector - Risks and Opportunities
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 User-aided Conjecturing for Automated Theorem Proving
AWS	Towards StarExec in the Cloud
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	Internship Opportunities in Mauritius, and Real-world Examples of AI Implementation in Business
BV	Deep Inference in Proof Search: The Need for Shallow Inference
C
Cached rewriting	Shared Terms and Cached Rewriting
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
Challenges	From Sugar Cane Fields to Cybercities: Data Science Bridging the Gap in Healthcare Access
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	Internship Opportunities in Mauritius, and Real-world Examples of AI Implementation in Business
concept alignment	Translating HOL-Light proofs to Coq
confluence	Confluence for Proof-Nets via Parallel Cut Elimination
Conjecturing	User-aided Conjecturing for Automated Theorem Proving
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
Containerisation	Towards StarExec in the Cloud
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
Data Science	From Sugar Cane Fields to Cybercities: Data Science Bridging the Gap in Healthcare Access
datalog	Fuzzy Datalog$^\exists$ over Arbitrary t-norms
Dataset-Specific	Dataset-Specific Strategies for the E Theorem Prover
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
E prover	Shared Terms and Cached Rewriting
E Theorem Prover	Dataset-Specific Strategies for the E Theorem Prover
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	Internship Opportunities in Mauritius, and Real-world Examples of AI Implementation in Business
Financial Services Sector	The Application of Artificial Intelligence in the Financial Services Sector - Risks and Opportunities
First Order Logic	Automated Theorem Provers Help Improve Large Language Model Reasoning
first-order theorem proving	Sorting without Sorts
FOL Provers	Invited talk: Hash Indexes for Resolution-based FOL Provers
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
Hash Indexes	Invited talk: Hash Indexes for Resolution-based FOL Provers
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
Human intuition	User-aided Conjecturing for Automated Theorem Proving
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	Internship Opportunities in Mauritius, and Real-world Examples of AI Implementation in Business
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
Kubernetes	Towards StarExec in the Cloud
L
lambda calculus	Hybrid Intersection Types for PCF
Large Language Models	Automated Theorem Provers Help Improve Large Language Model Reasoning
Limited Resources	Transfer Learning Hacks for Small Data Context: Enhancing Recommendation Systems with Limited Resources
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	From Sugar Cane Fields to Cybercities: Data Science Bridging the Gap in Healthcare Access Internship Opportunities in Mauritius, and Real-world Examples of AI Implementation in Business
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
Opportunities	The Application of Artificial Intelligence in the Financial Services Sector - Risks and Opportunities
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
Recommendation Systems	Transfer Learning Hacks for Small Data Context: Enhancing Recommendation Systems with Limited Resources
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
Resolution-based	Invited talk: Hash Indexes for Resolution-based FOL Provers
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
Risks	The Application of Artificial Intelligence in the Financial Services Sector - Risks and Opportunities
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
Shared terms	Shared Terms and Cached Rewriting
simulation	Efficient Simulation for Hardware Model Checking
Skolemization	A Generic Deskolemization Strategy
Small Data	Transfer Learning Hacks for Small Data Context: Enhancing Recommendation Systems with Limited Resources
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	Internship Opportunities in Mauritius, and Real-world Examples of AI Implementation in Business
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
StarExec	Towards StarExec in the Cloud
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
Strategies	Dataset-Specific Strategies for the E Theorem Prover
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	The Potential and Future of AI in the Medical Field Creating Real-life Homologous Environments for Deep Reinforcement Learning The State of AI in Mauritius: Academic and Private Sector Perspectives Consumer Predictive Model using Sentiment Analysis Mauritius as a Burgeoning AI Hub and Way Forward
TBA2	The Potential and Future of AI in the Medical Field Creating Real-life Homologous Environments for Deep Reinforcement Learning The State of AI in Mauritius: Academic and Private Sector Perspectives Consumer Predictive Model using Sentiment Analysis Mauritius as a Burgeoning AI Hub and Way Forward
TBA3	The Potential and Future of AI in the Medical Field Creating Real-life Homologous Environments for Deep Reinforcement Learning The State of AI in Mauritius: Academic and Private Sector Perspectives Consumer Predictive Model using Sentiment Analysis Mauritius as a Burgeoning AI Hub and Way Forward
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
Transfer Learning	Transfer Learning Hacks for Small Data Context: Enhancing Recommendation Systems with Limited Resources
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.