Lemmaless induction in trace logic

DOI10.1007/978-3-031-16681-5_14MaRDI QIDQ6160563zbMATH OpenOpenAlexFDO

Authors Ahmed Bhayat, Pamina Georgiou, Clemens Eisenhofer, Laura Kovács, Giles Reger

Publication date 2 June 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-16681-5_14

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Recommendations

• scientific article; zbMATH DE number 2174388
• On induction-free provability
• scientific article; zbMATH DE number 638309
• Automatic proofs by induction in theories without constructors
• Logical definability on infinite traces
• Logical definability on infinite traces
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
• Deductively definable logics of induction
• Induction in linear logic
• Trace semantics via determinization

Cites work

• \textsc{Diffy}: inductive reasoning of array programs using difference invariants
• Automating Inductive Proofs Using Theory Exploration
• Coming to terms with quantified reasoning
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• Dafny: an automatic program verifier for functional correctness
• Integer induction in saturation
• Integrating Linear Arithmetic into Superposition Calculus
• Making theory reasoning simpler
• Quantified invariants via syntax-guided synthesis
• Quantifiers on demand
• Resolution theorem proving
• SMT-based array invariant generation
• Verifying array manipulating programs with full-program induction

This page was built for publication: Lemmaless induction in trace logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6160563)