scientific article; zbMATH DE number 7178358

MaRDI QIDQ5219923zbMATH OpenFDO

Authors Clark Barrett, Leonardo de Moura, Pascal Fontaine

Publication date 9 March 2020

Mathematics Subject Classification ID

Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited in

(5)

• Flexible proof production in an industrial-strength SMT solver
• Scalable fine-grained proofs for formula processing
• Proof-carrying neuro-symbolic code
• A certified proof checker for deep neural network verification in imandra
• Towards a trustworthy semantics-based language framework via proof generation

Describes a project that uses

Uses Software

• Isabelle/HOL
• SMT-LIB
• veriT
• CVC Lite
• MathSAT
• Lean
• z3
• HOL Light
• CVC
• CVC4

This page was built for publication:

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