Induction for SMT Solvers

DOI10.1007/978-3-662-46081-8_5zbMath1432.68418OpenAlexW1856554806MaRDI QIDQ5172636

Viktor Kuncak, Andrew Reynolds

Publication date: 4 February 2015

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

Full work available at URL: https://doi.org/10.1007/978-3-662-46081-8_5

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

A decision procedure for (co)datatypes in SMT solvers, Verifying Catamorphism-Based Contracts using Constrained Horn Clauses, Contract-based verification of MATLAB-style matrix programs, Inductive benchmarks for automated reasoning, Theory exploration powered by deductive synthesis, TIP: Tons of Inductive Problems, A Decision Procedure for (Co)datatypes in SMT Solvers, Generalized arrays for Stainless frames, Analysis and Transformation of Constrained Horn Clauses for Program Verification, Getting saturated with induction, Reasoning about algebraic data types with abstractions, Solving constrained Horn clauses over algebraic data types, Unnamed Item, Unnamed Item, Unnamed Item, Bridging arrays and ADTs in recursive proofs, Combining induction and saturation-based theorem proving, Integer induction in saturation, Induction in saturation-based proof search, CVC4, Induction and Skolemization in saturation theorem proving, Removing algebraic data types from constrained Horn clauses using difference predicates