A |

abstract interpretation | Automatic Detection of Vulnerable Variables for CTL Properties of Programs |

action model | Symbolic Realisation of Epistemic Processes |

arithmetic | VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic |

automated inductive reasoning | Saturating Sorting without Sorts |

automated reasoning | Saturating Sorting without Sorts Scaling CheckMate for Game-Theoretic Security First Experiments with Neural cvc5 |

automated software verification | Saturating Sorting without Sorts |

automated theorem proving | Automated Theorem Provers Help Improve Large Language Model Reasoning Saturating Sorting without Sorts Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper) A Generic Deskolemization Strategy Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery |

B |

bags | Verifying SQL queries using theories of tables and relations |

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 |

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 | Translating HOL-Light proofs to Coq Certifying Incremental SAT Solving |

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 |

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 |

constraint solving | Minimizing Sorting Networks at the Sub-Comparator Level |

CTL | Automatic Detection of Vulnerable Variables for CTL Properties of Programs |

cut elimination | Confluence for Proof-Nets via Parallel Cut Elimination |

D |

Datalog | Fuzzy Datalog∃ 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 |

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 strategies | Hybrid Intersection Types for PCF |

F |

first-order logic | Automated Theorem Provers Help Improve Large Language Model Reasoning |

first-order theorem proving | Saturating Sorting without Sorts |

formal methods | Saturating Sorting without Sorts |

Free-Variable Tableaux | A Generic Deskolemization Strategy |

Fuzzy Logic | Fuzzy Datalog∃ 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 |

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 |

intersection types | Hybrid Intersection Types for PCF |

K |

knowledge representation | A Tool for Reasoning about Trust and Belief |

L |

lambda calculus | Hybrid Intersection Types for PCF |

large language models | Automated Theorem Provers Help Improve Large Language Model Reasoning |

linear logic | A Simple Token Game and its Logic Confluence for Proof-Nets via Parallel Cut Elimination |

LIRA | VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic |

logic programming | Automated Theorem Provers Help Improve Large Language Model Reasoning |

logical frameworks | Translating HOL-Light proofs to Coq |

M |

machine learning | First Experiments with Neural cvc5 |

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 |

monadic second-order logic | Tree-Verifiable Graph Grammars |

N |

natural language | Automated Theorem Provers Help Improve Large Language Model Reasoning |

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 |

NP-hardness | Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition |

P |

parallel reduction | Confluence for Proof-Nets via Parallel Cut Elimination |

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 |

program optimization | Minimizing Sorting Networks at the Sub-Comparator Level |

program verification | Automatic Detection of Vulnerable Variables for CTL Properties of Programs Automatic Bit- and Memory-Precise Verification of eBPF Code |

proof certificate | A Generic Deskolemization Strategy |

proof checking | Certifying Incremental SAT Solving |

Proof Schema | Herbrand's Theorem in Inductive Proofs |

proof search | Deep Inference in Proof Search: The Need for Shallow Inference |

proof theory | A Simple Token Game and its Logic |

proof transformation | Translating HOL-Light proofs to Coq |

proof translation | Translating HOL-Light proofs to Coq Experiments with Choice in Dependently-Typed Higher-Order Logic |

proof-net | Confluence for Proof-Nets via Parallel Cut Elimination |

Proof-Search Procedures | A Generic Deskolemization Strategy |

proofs | Certifying Incremental SAT Solving |

propositional dynamic logic | Symbolic Realisation of Epistemic Processes |

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 |

R |

Reasoning | Automated Theorem Provers Help Improve Large Language Model Reasoning |

recursive programs | Saturating Sorting without Sorts |

relations | Verifying SQL queries using theories of tables and relations |

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 | Translating HOL-Light proofs to Coq Rewriting and Inductive Reasoning |

S |

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 |

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 |

sequent calculus | On Translations of Epsilon Proofs to LK |

sequent system | Reasoning About Group Polarization: From Semantic Games to Sequent Systems |

sets | Verifying SQL queries using theories of tables and relations |

simulation | Efficient Simulation for Hardware Model Checking |

Skolemization | A Generic Deskolemization Strategy |

SMT | VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic Verifying SQL queries using theories of tables and relations |

sorting algorithms | Saturating Sorting without Sorts |

sorting networks | Minimizing Sorting Networks at the Sub-Comparator Level |

SQL | Verifying SQL queries using theories of tables and relations |

static analysis | Automatic Detection of Vulnerable Variables for CTL Properties of Programs Automated Synthesis of Decision Lists for Polynomial Specifications over Integers |

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 | Saturating Sorting without Sorts |

symbolic abstraction | Symbolic Realisation of Epistemic Processes |

symbolic execution | Symbolic Realisation of Epistemic Processes |

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 |

theorem proving | First Experiments with Neural cvc5 |

theory combination | Combining Combination Properties: Minimal Models |

Theory Politeness | Combining Combination Properties: Minimal Models |

Trust | A Tool for Reasoning about Trust and Belief |

Tuple-generating dependencies | Fuzzy Datalog∃ over Arbitrary t-Norms |

V |

verification | Efficient Simulation for Hardware Model Checking |

virtual substitution | VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic |

W |

weakest liberal precondition | Symbolic Realisation of Epistemic Processes |