/usr/share/doc/libghc-sbv-doc/html/Data-SBV-Examples-Uninterpreted-Deduce.html

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Data.SBV.Examples.Uninterpreted.Deduce</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Data-SBV-Examples-Uninterpreted-Deduce.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">sbv-5.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Copyright</th><td>(c) Levent Erkok</td></tr><tr><th>License</th><td>BSD3</td></tr><tr><th>Maintainer</th><td>erkokl@gmail.com</td></tr><tr><th>Stability</th><td>experimental</td></tr><tr><th>Safe Haskell</th><td>None</td></tr><tr><th>Language</th><td>Haskell2010</td></tr></table><p class="caption">Data.SBV.Examples.Uninterpreted.Deduce</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">Representing uninterpreted booleans</a></li><li><a href="#g:2">Uninterpreted connectives over <code>B</code></a></li><li><a href="#g:3">Axioms of the logical system</a></li><li><a href="#g:4">Demonstrated deduction</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Demonstrates uninterpreted sorts and how they can be used for deduction.
 This example is inspired by the discussion at <a href="http://stackoverflow.com/questions/10635783/using-axioms-for-deductions-in-z3">http://stackoverflow.com/questions/10635783/using-axioms-for-deductions-in-z3</a>,
 essentially showing how to show the required deduction using SBV.</p></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">data</span> <a href="#t:B">B</a> = <a href="#v:B">B</a> ()</li><li class="src short"><span class="keyword">type</span> <a href="#t:SB">SB</a> = <a href="Data-SBV-Internals.html#t:SBV">SBV</a> <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></li><li class="src short"><a href="#v:and">and</a> :: <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> -&gt; <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> -&gt; <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a></li><li class="src short"><a href="#v:or">or</a> :: <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> -&gt; <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> -&gt; <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a></li><li class="src short"><a href="#v:not">not</a> :: <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> -&gt; <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a></li><li class="src short"><a href="#v:ax1">ax1</a> :: [<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-String.html#t:String">String</a>]</li><li class="src short"><a href="#v:ax2">ax2</a> :: [<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-String.html#t:String">String</a>]</li><li class="src short"><a href="#v:ax3">ax3</a> :: [<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-String.html#t:String">String</a>]</li><li class="src short"><a href="#v:test">test</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a></li></ul></div><div id="interface"><h1 id="g:1">Representing uninterpreted booleans</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:B" class="def">B</a> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#B" class="link">Source</a></p><div class="doc"><p>The uninterpreted sort <code><a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></code>, corresponding to the carrier.
 To prevent SBV from translating it to an enumerated type, we simply attach an unused field</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:B" class="def">B</a> ()</td><td class="doc empty">&nbsp;</td></tr></table></div><div class="subs instances"><p id="control.i:B" class="caption collapser" onclick="toggleSection('i:B')">Instances</p><div id="section.i:B" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Eq.html#t:Eq">Eq</a> <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></span> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#line-32" class="link">Source</a></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src clearfix"><span class="inst-left"><a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Data.html#t:Data">Data</a> <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></span> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#line-32" class="link">Source</a></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src clearfix"><span class="inst-left"><a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Ord.html#t:Ord">Ord</a> <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></span> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#line-32" class="link">Source</a></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src clearfix"><span class="inst-left"><a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Text-Read.html#t:Read">Read</a> <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></span> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#line-32" class="link">Source</a></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src clearfix"><span class="inst-left"><a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Text-Show.html#t:Show">Show</a> <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></span> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#line-32" class="link">Source</a></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src clearfix"><span class="inst-left"><a href="Data-SBV-Internals.html#t:HasKind">HasKind</a> <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></span> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#line-32" class="link">Source</a></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src clearfix"><span class="inst-left"><a href="Data-SBV.html#t:SymWord">SymWord</a> <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></span> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#line-32" class="link">Source</a></td><td class="doc empty">&nbsp;</td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:SB" class="def">SB</a> = <a href="Data-SBV-Internals.html#t:SBV">SBV</a> <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#SB" class="link">Source</a></p><div class="doc"><p>Handy shortcut for the type of symbolic values over <code><a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></code></p></div></div><h1 id="g:2">Uninterpreted connectives over <code><a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></code></h1><div class="top"><p class="src"><a name="v:and" class="def">and</a> :: <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> -&gt; <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> -&gt; <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#and" class="link">Source</a></p><div class="doc"><p>Uninterpreted logical connective <code><a href="Data-SBV-Examples-Uninterpreted-Deduce.html#v:and">and</a></code></p></div></div><div class="top"><p class="src"><a name="v:or" class="def">or</a> :: <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> -&gt; <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> -&gt; <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#or" class="link">Source</a></p><div class="doc"><p>Uninterpreted logical connective <code><a href="Data-SBV-Examples-Uninterpreted-Deduce.html#v:or">or</a></code></p></div></div><div class="top"><p class="src"><a name="v:not" class="def">not</a> :: <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> -&gt; <a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:SB">SB</a> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#not" class="link">Source</a></p><div class="doc"><p>Uninterpreted logical connective <code><a href="Data-SBV-Examples-Uninterpreted-Deduce.html#v:not">not</a></code></p></div></div><h1 id="g:3">Axioms of the logical system</h1><div class="top"><p class="src"><a name="v:ax1" class="def">ax1</a> :: [<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-String.html#t:String">String</a>] <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#ax1" class="link">Source</a></p><div class="doc"><p>Distributivity of OR over AND, as an axiom in terms of
 the uninterpreted functions we have introduced. Note how
 variables range over the uninterpreted sort <code><a href="Data-SBV-Examples-Uninterpreted-Deduce.html#t:B">B</a></code>.</p></div></div><div class="top"><p class="src"><a name="v:ax2" class="def">ax2</a> :: [<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-String.html#t:String">String</a>] <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#ax2" class="link">Source</a></p><div class="doc"><p>One of De Morgan's laws, again as an axiom in terms
 of our uninterpeted logical connectives.</p></div></div><div class="top"><p class="src"><a name="v:ax3" class="def">ax3</a> :: [<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-String.html#t:String">String</a>] <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#ax3" class="link">Source</a></p><div class="doc"><p>Double negation axiom, similar to the above.</p></div></div><h1 id="g:4">Demonstrated deduction</h1><div class="top"><p class="src"><a name="v:test" class="def">test</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/System-IO.html#t:IO">IO</a> <a href="Data-SBV.html#t:ThmResult">ThmResult</a> <a href="src/Data-SBV-Examples-Uninterpreted-Deduce.html#test" class="link">Source</a></p><div class="doc"><p>Proves the equivalence <code>NOT (p OR (q AND r)) == (NOT p AND NOT q) OR (NOT p AND NOT r)</code>,
 following from the axioms we have specified above. We have:</p><pre class="screen"><code class="prompt">&gt;&gt;&gt; </code><strong class="userinput"><code>test
</code></strong>Q.E.D.
</pre></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.16.1</p></div></body></html>
libghc-sbv-doc 5.9-1build1 / usr / share / doc / libghc-sbv-doc / html / Data-SBV-Examples-Uninterpreted-Deduce.html
