| a |
| autoformalization | Representation Abstraction and Proof Search for English-to-Logic Question Answering |
| automata theory | Blinking Synthesis |
| automated reasoning | Formally Solving Answer-Construction Problems in Lean
Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Thousands of Problems to Lean |
| automated theorem proving | Reasoning About Hyperproperties with Automated Theorem Provers
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
Representation Abstraction and Proof Search for English-to-Logic Question Answering |
| axiomatization | Comparison Invariants for Verifying Control Invariance |
| b |
| Benchmarks | Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB
Reasoning About Hyperproperties with Automated Theorem Provers |
| Boltzmann machines | Formalized Hopfield Networks and Boltzmann Machines |
| Boolos' curious inference | Experiments on Automating Boolos' Curious Inference |
| branching vector addition systems | Tight Complexity for Modal Extensions of Lec with K, 4, T |
| c |
| Calculus of Inductive Constructions | Aligning HOL-Light and Rocq Libraries Formally
A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions |
| cardinality constraints | Coloring Queens with Thousands of Encodings |
| CDCL | Extending SMT Solving with Non-Ground Clause Learning |
| CEGAR | Compact Partial Symmetry Breaking for Graph Search Problems |
| circuit equivalences | Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB |
| Claude Code | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq |
| commonsense reasoning | Representation Abstraction and Proof Search for English-to-Logic Question Answering |
| comparison invariants | Comparison Invariants for Verifying Control Invariance |
| Comparison systems | Comparison Invariants for Verifying Control Invariance |
| complementation | Simple Complementation of Generalized Büchi Automata |
| computational complexity | Subsumption in FL_⊥reg with TBox Is in ExpTime.
Tight Complexity for Modal Extensions of Lec with K, 4, T |
| control invariance | Comparison Invariants for Verifying Control Invariance |
| cut-introduction | Experiments on Automating Boolos' Curious Inference |
| Cyber-Physical Systems | STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas |
| d |
| de Vrijer's measure | de Vrijer's Strong Normalization in Haskell |
| decidable fragments | Maslov's class K with Equivalence |
| defeasible reasoning | Representation Abstraction and Proof Search for English-to-Logic Question Answering |
| dependent types | A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions |
| Description Logic | Subsumption in FL_⊥reg with TBox Is in ExpTime. |
| differential dynamic logic | Comparison Invariants for Verifying Control Invariance |
| e |
| eigenvariable conditions | First-Order Tableaux with Unification for Henkin Quantifiers |
| English-to-logic translation | Representation Abstraction and Proof Search for English-to-Logic Question Answering |
| EPR | Reintroducing the Second Player in EPR |
| equational theories | A SAT Attack on Tarski's High School Algebra Problem |
| equivalence relations | Maslov's class K with Equivalence |
| Event Calculus | Stream Reasoning with Sequencing |
| f |
| finite model property | Maslov's class K with Equivalence |
| first-order logic | Maslov's class K with Equivalence |
| first-order theorem proving | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification |
| formal mathematics | Formalized Hopfield Networks and Boltzmann Machines |
| formal methods | Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean |
| g |
| Generalized Büchi Automata | Simple Complementation of Generalized Büchi Automata |
| Google Gemini | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq |
| graph coloring | Coloring Queens with Thousands of Encodings |
| graph symmetry | Compact Partial Symmetry Breaking for Graph Search Problems |
| greedy runs | Simple Complementation of Generalized Büchi Automata |
| h |
| Henkin quantifiers | First-Order Tableaux with Unification for Henkin Quantifiers |
| high school identities | A SAT Attack on Tarski's High School Algebra Problem |
| Higher order moments | Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support |
| higher-order logic | Aligning HOL-Light and Rocq Libraries Formally
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
Experiments on Automating Boolos' Curious Inference |
| Hopfield networks | Formalized Hopfield Networks and Boltzmann Machines |
| Hybrid modal logic | Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean |
| hyperltl | Induction and K-Induction for Hyperproperties |
| Hyperproperties | Reasoning About Hyperproperties with Automated Theorem Provers |
| i |
| imperfect information | Blinking Synthesis |
| induction | Induction and K-Induction for Hyperproperties |
| infinite-state systems | Tight Complexity for Modal Extensions of Lec with K, 4, T |
| interactive theorem proving | Thousands of Problems to Lean
Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean |
| invariant synthesis | Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support |
| ITP hammers | Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection |
| k |
| k-induction | Induction and K-Induction for Hyperproperties |
| knowledge representation | Stream Reasoning with Sequencing
Representation Abstraction and Proof Search for English-to-Logic Question Answering |
| l |
| large language models | Formally Solving Answer-Construction Problems in Lean
LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
Representation Abstraction and Proof Search for English-to-Logic Question Answering |
| Lean 4 | Formally Solving Answer-Construction Problems in Lean
Thousands of Problems to Lean
Formalized Hopfield Networks and Boltzmann Machines
Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean |
| library alignment | Aligning HOL-Light and Rocq Libraries Formally |
| linear arithmetic | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification |
| literal selection | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification |
| logic and types | Thousands of Problems to Lean |
| m |
| many-sorted signatures | Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean |
| martingale | Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support |
| Maslov's class K | Maslov's class K with Equivalence |
| mathlib | Formalized Hopfield Networks and Boltzmann Machines |
| modal logic | Tight Complexity for Modal Extensions of Lec with K, 4, T
Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean |
| model checking | Induction and K-Induction for Hyperproperties
Reasoning About Hyperproperties with Automated Theorem Provers |
| multiplicative substructural logic | Tight Complexity for Modal Extensions of Lec with K, 4, T |
| n |
| natural language | Representation Abstraction and Proof Search for English-to-Logic Question Answering |
| neural clause-selection guidance | Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection |
| neural networks | Formalized Hopfield Networks and Boltzmann Machines |
| o |
| optional stopping | Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support |
| p |
| pattern matching | A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions |
| PhysLib | Formalized Hopfield Networks and Boltzmann Machines |
| probabilistic programs | Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support |
| program verification | Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support |
| proof checking | Scaling Zero Knowledge UNSAT Verification via Normalized Chaining |
| proof length | Experiments on Automating Boolos' Curious Inference |
| proof verification | Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic |
| proving strategies | Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection |
| PSPACE | Reintroducing the Second Player in EPR |
| Pushdown Games | Subsumption in FL_⊥reg with TBox Is in ExpTime. |
| q |
| QBF | Reintroducing the Second Player in EPR |
| queen's graph | Coloring Queens with Thousands of Encodings |
| Question Answering | Representation Abstraction and Proof Search for English-to-Logic Question Answering |
| r |
| Ramsey graphs | Compact Partial Symmetry Breaking for Graph Search Problems |
| reachability | Tight Complexity for Modal Extensions of Lec with K, 4, T |
| real arithmetic | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification |
| redundancy | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification |
| Requirements Engineering | STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas |
| Rocq | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions |
| s |
| SAT | A SAT Attack on Tarski's High School Algebra Problem |
| SAT encoding | Coloring Queens with Thousands of Encodings |
| satisfiability | STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
Maslov's class K with Equivalence |
| saturation-based theorem proving | Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection |
| Schaefer fragments | Reintroducing the Second Player in EPR |
| SCL | Extending SMT Solving with Non-Ground Clause Learning |
| Signal Temporal Logic | STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas |
| simply typed lambda calculus | de Vrijer's Strong Normalization in Haskell |
| SMT | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB
Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Reasoning About Hyperproperties with Automated Theorem Provers
Extending SMT Solving with Non-Ground Clause Learning |
| software verification | Reasoning About Hyperproperties with Automated Theorem Provers |
| Stream Reasoning | Stream Reasoning with Sequencing |
| strong normalization | de Vrijer's Strong Normalization in Haskell |
| superposition | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification |
| symmetry breaking | Coloring Queens with Thousands of Encodings |
| synthesis of reactive systems | Blinking Synthesis |
| t |
| tableau methods | STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
First-Order Tableaux with Unification for Henkin Quantifiers |
| theorem proving | Formally Solving Answer-Construction Problems in Lean |
| TPTP | Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB |
| Tree-shaped Tableau | STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas |
| type theory | Formalized Hopfield Networks and Boltzmann Machines |
| v |
| Vampire | Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection |
| w |
| Wilkie's identity | A SAT Attack on Tarski's High School Algebra Problem |
| z |
| zero-knowledge proofs | Scaling Zero Knowledge UNSAT Verification via Normalized Chaining |
