Home // COMPUTATION TOOLS 2011, The Second International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking // View article
Authors:
Lev Naiman
Eric Hehner
Keywords: proof, calculation, tool
Abstract:
Netty is a prover’s assistant. It supports a calcula- tional style of proof, and allows the creation of proofs that are correct by construction. It provides an intuitive interface that allows direct manipulation of expressions. The key idea is that instead of tactics for proof the user only needs to select the next step of the proof from a list of suggestions. These suggestions are usually the result of unification. Netty provides mechanisms to facilitate proving, such as making use of local assumptions and the use of monotonicity in subproofs. Program refinement from specification can be done in Netty similarly to any other kind of proof.
Pages: 1 to 6
Copyright: Copyright (c) IARIA, 2011
Publication date: September 25, 2011
Published in: conference
ISSN: 2308-4170
ISBN: 978-1-61208-159-5
Location: Rome, Italy
Dates: from September 25, 2011 to September 30, 2011