System description: IVY

DOI10.1007/10721959_30MaRDI QIDQ2723435zbMATH OpenFDO

Authors Olga Shumsky, William McCune

Publication date 5 July 2001

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

Full work available at URL https://doi.org/10.1007/10721959_30

Mathematics Subject Classification ID

Recommendations

• Deductive verification in decidable fragments with Ivy
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• System description: E 1.8
• Theorem Proving in Higher Order Logics
• Computer Aided Verification

Cited in

(8)

• Varieties of regular semigroups with uniquely defined inversion
• Ivy
• Extending Sledgehammer with SMT solvers
• Theorem proving in large theories
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• A method for proving ITL theorem by using PVS
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• scientific article; zbMATH DE number 1552508 (Why is no real title available?)

Describes a project that uses

Uses Software

• OTTER
• Mace4
• ACL2

This page was built for publication: System description: IVY

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