| 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 |
