Generalizes PDL to OPDL by distinguishing programs from traces via arbitrary operational semantics and proves cut-elimination for a non-wellfounded sequent calculus.
Title resolution pending
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
verdicts
UNVERDICTED 3representative citing papers
Unrolling heuristic for recursive functions is complete for first-order theories of algebraic datatypes combined with decidable quantifier-free background theories.
An agentic theorem prover in Lean uses a control plane to route actions based on cost and success estimates, achieving 28.9% lower average cost than a fixed-step baseline on a PutnamBench subset while preserving performance.
citing papers explorer
-
On Propositional Dynamic Logic and Concurrency
Generalizes PDL to OPDL by distinguishing programs from traces via arbitrary operational semantics and proves cut-elimination for a non-wellfounded sequent calculus.
-
Complete first-order reasoning for functional programs
Unrolling heuristic for recursive functions is complete for first-order theories of algebraic datatypes combined with decidable quantifier-free background theories.
-
Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
An agentic theorem prover in Lean uses a control plane to route actions based on cost and success estimates, achieving 28.9% lower average cost than a fixed-step baseline on a PutnamBench subset while preserving performance.