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 |