Polynomial Lawvere Logic
CoRR(2024)
摘要
In this paper, we study Polynomial Lawvere logic (PL), a logic on the
quantale of the extended positive reals, developed for reasoning about metric
spaces. PL is appropriate for encoding quantitative reasoning principles, such
as quantitative equational logic. PL formulas include the polynomial functions
on the extended positive reals, and its judgements include inequalities between
polynomials.
We present an inference system for PL and prove a series of completeness and
incompleteness results relying and the Krivine-Stengle Positivstellensatz (a
variant of Hilbert's Nullstellensatz) including completeness for finitely
axiomatisable PL theories.
We also study complexity results both for both PL and its affine fragment
(AL). We demonstrate that the satisfiability of a finite set of judgements is
NP-complete in AL and in PSPACE for PL; and that deciding the semantical
consequence from a finite set of judgements is co-NP complete in AL and in
PSPACE in PL.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要