An even closer integration of linear arithmetic into inductive theorem proving
From MaRDI portal
Recommendations
- New uses of linear arithmetic in automated theorem proving by induction
- Proof synthesis and reflection for linear arithmetic
- scientific article; zbMATH DE number 4112064
- Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL
- Tools and Algorithms for the Construction and Analysis of Systems
- Proofs as computations in linear logic
- scientific article; zbMATH DE number 1222110
- Proving equational and inductive theorems by completion and embedding techniques
- An integral theorem prover and the role of proof planning
- scientific article; zbMATH DE number 1292302
Cited in
(9)- Using an induction prover for verifying arithmetic circuits
- New uses of linear arithmetic in automated theorem proving by induction
- \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Integration of linear arithmetic and goal-oriented resolution for software reasoning
- Shallow confluence of conditional term rewriting systems
- Producing proofs from an arithmetic decision procedure in elliptical LF
- scientific article; zbMATH DE number 4112064 (Why is no real title available?)
- Linear strategy for Boolean ring based theorem proving
This page was built for publication: An even closer integration of linear arithmetic into inductive theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2852038)
