Coming to terms with quantified reasoning

DOI10.1145/3009837.3009887zbMath1380.68280arXiv1611.02908OpenAlexW2563639488MaRDI QIDQ5370860

Laura Kovács, Andrei Voronkov, Simon Robillard

Publication date: 20 October 2017

Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1611.02908

zbMATH Keywords

automated reasoningprogram analysisprogram verificationalgebraic data typesfirst-order theorem provingsuperposition proving

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (10)

A First-Order Logic with Frames ⋮ Getting saturated with induction ⋮ Lemmaless induction in trace logic ⋮ Integer induction in saturation ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ Induction in saturation-based proof search ⋮ Polite combination of algebraic datatypes ⋮ Politeness for the theory of algebraic datatypes ⋮ Layered clause selection for theory reasoning (short paper) ⋮ MedleySolver: online SMT algorithm selection

Uses Software

• Isabelle/HOL
• VAMPIRE
• SMT-LIB
• z3
• CVC4
• E Theorem Prover
• HALO

This page was built for publication: Coming to terms with quantified reasoning