https://prooftoys.org/about/

1<!DOCTYPE html>
2
3
4
5<html lang="en" class=logicZone>
6<head>
7  <meta charset="utf-8">
8  <meta http-equiv="x-ua-compatible" content="ie=edge">
9  <title>About - Prooftoys</title>
10  <meta name="viewport" content="width=device-width, initial-scale=1">
11  <meta name=description content="Prooftoys is a simple, easy to learn and use use proof assistant for beginners.">
12  
13  <link rel="icon" href="/favicon.ico">
14  
15  
16  
17  <style>
18  [class*=" fa-"]::before {
19    content:"\2606";
20  }
21  </style>
22  
23  <link rel="stylesheet" href="/css/style.css">
24
25  
26  
27  <link rel="stylesheet" href="/css/pt.css">
28  
29
30  
31  <style type="text/css">
32  .logicZone .docs-menu ul a[href="/about/"] {
33      background-color: lightgreen;
34  }
35  .tippy-box {
36    background-color: darkolivegreen;
37  }
38  .tippy-arrow {
39    color: darkolivegreen;
40  }
41  </style>
42

43<script src="https://code.jquery.com/jquery-3.6.0.js"></script>

43
44
45

46<script type="text/javascript">
47  
48  
49  
50  var _paq = window._paq = window._paq || [];
51(function() {
52  
53  
54  var mappings = [
55    [/^prooftoys.org$/, 1],
56    [/^mathtoys.org$/, 3],
57    [/^perdues.com$/, 4],
58    
59    [/^localhost:/, null],
60    
61    
62    [/:|netlify.app$/, 6],
63  ];
64  var id = null;
65  for (var i = 0; i < mappings.length; i++) {
66    var entry = mappings[i];
67    if (location.host.match(entry[0])) {
68      id = entry[1];
69      if (id) {
70        
71        
72        
73        _paq.push(['disableCookies']);
74        
75        
76        _paq.push(['trackPageView']);
77        _paq.push(['enableLinkTracking']);
78        
79        
80        
81        
82        _paq.push(['setTrackerUrl', 'https://prooftoys.org/m.php']);
83        _paq.push(['setSiteId', id]);
84        
85        
86        var uxOK = localStorage.getItem('Toy:uxOK') === 'true';
87        if (!uxOK) {
88          
89          _paq.push(['HeatmapSessionRecording::disable']);
90          console.log('Session recording OFF')
91        }
92        var d=document, g=d.createElement('script'),
93            s=d.getElementsByTagName('script')[0];
94        g.type='text/javascript';
95        g.async=true;
96        
97        g.src = '//cdn.matomo.cloud/prooftoys.matomo.cloud/matomo.js'
98        
99        g.src = '//prooftoys.org/m.js';
100        s.parentNode.insertBefore(g,s);
101      }
102      
103      break;
104    }
105  }
106  if (!id) {
107    
108    _paq = null;
109  }
110})();
111</script>

111
112
113
114</head>
115
116<body class=''>
117
118<header class="nav-links">
119  <a href="/">
120    <img src="/Logo1.svg">
121  </a>
122  <a href="/hands-on/"><img class="icon" src="/DIY.svg"></a>
123  <a href="/preview/"><img class="icon" src="/Sneak Preview.svg"></a>
124  <span class="fill">&nbsp;</span>
125  <a href="/documentation/">Docs</a>
126  <a href="/mission/">Mission</a>
127  <a href="/about/">About</a>
128</header>
129
130  
131  
132  
133    <div class="main-row row ml-1 mr-1 mt-7">
134      <div style="text-align: left">
135        
136<button id="toggle-main-menu-mobile"
137 class="hamburger hamburger--slider"
138 type="button">
139  <span class="hamburger-box">
140    <span class="hamburger-inner"></span>
141  </span>&nbsp;&nbsp;Links
142</button>
143
144      </div>
145      <div class="col-12 col-md-4 col-lg-3">
146	      <div class="sidebar floating ">
147	        <div class="docs-menu mb-3">
148
149  
150
151</div>
152
153	      </div>
154      </div>
155      <div class="col-12 col-md-8 col-lg-9">
156	      
157<section id="main">
158  <blockquote>
159<p>The scientific man does not aim at an immediate result.  He does not
160expect that his advanced ideas will be readily taken up.  His work is
161like that of the planter &ndash; for the future.  His duty is to lay the
162foundation for those who are to come, and point the way. &mdash; Nikola
163Tesla</p>
164</blockquote>
165<h3 id="about-prooftoysorg">About Prooftoys.org</h3>
166<p><strong>Welcome!</strong> The <a href="http://prooftoys.org">Prooftoys</a> website and its
167software are ongoing experiments in creating computer aids to help
168human beings learn and do mathematics.  The application software is
169proudly open source, hosted at <a href="http://github.com">Github</a>,
170primarily in the <a
171href="http://github.com/crisperdue/prooftoys">crisperdue/prooftoys</a>
172repository.</p>
173<p>The key goal is to create a computer math tool or tools that are easy,
174highly available, useful, attractive, and valuable to people learning
175(or doing) mathematics, especially newcomers, for reading and writing
176proofs, and for solving problems deductively.</p>
177<p>The larger vision is to develop the kind of user experience that can
178bridge the gap between computer proof technology and ordinary people
179learning to understand and use mathematics.</p>
180<h3 id="about-the-logic">About the logic</h3>
181<p>At its core, the reasoning in Prooftoys is <strong>equational</strong>, in other
182words based on equations.  In particular Leibniz&rsquo;s principle of
183replacing a term with an equal term is fundamental, as applied in
184algebra from the basic high school level and up.</p>
185<p>Prooftoys implements a form of logic known as <a target=_blank href=
186"https://imps.mcmaster.ca/doc/seven-virtues.pdf">simple type theory</a>.
187Anything provable in &ldquo;first-order&rdquo; logic remains provable.  Furthermore,
188reasoning about equality is not an add-on, in fact it is the core.
189General statements about functions and predicates can also be expressed
190and proved here, unlike first-order logic.</p>
191<p>This particular system is based rather directly on the
192<strong>Q<sub>0</sub></strong> system of Carnegie Mellon University Professor Peter B.
193Andrews.  See the <a href="/tech-notes/">tech notes</a> for more
194details.</p>
195<h3 id="working-with-a-logic-textbook">Working with a logic textbook</h3>
196<p>Yes, you should be able to use the Proof Builder tool with your logic
197textbook.  If your textbook presents problems to solve by formally
198proving or disproving statements in pure logic, the intention is that
199you will solve the problems using the rules laid out in the textbook.</p>
200<p>To do this, you will need to be careful to limit the inference steps and
201logic facts you use.  <a href="/emulating-logics/">This page</a>
202has details for a couple of examples I have seen reference.</p>
203<h3 id="getting-in-touch">Getting in touch</h3>
204<p>One goal is to develop a friendly community of users around the tools
205here and their goals of using computers for mathematical reasoning.
206Don&rsquo;t hesitate to say &ldquo;hello&rdquo; to the author through <a
207href="mailto:[email protected]"><b>email</b></a>.</p>
208<p>Sincerely,<br>
209Cris Perdue</p>
210<!--
211Or you can reach him on Slack.com with <a target=_blank href=
212"https://join.slack.com/t/prooftoys/shared_invite/zt-hfjkerk4-Am67OX60KEHycW9WEKFbxQ">
213<b>this link</b></a>.
214
215Today there are wonderful tools for practitioners who need answers to
216mathematical questions, ranging from handheld calculators to numerical
217simulators to computer algebra systems.  Generally speaking, these
218tools do not require their users to use proof, though understanding of
219mathematical principles can be most helpful to users of these tools,
220and proof is a part of the essence of all mathematical principles.
221
222At the same time, mathematical proof is poorly understood by both
223students and skilled practitioners of fields that use and even rely on
224mathematics.
225
226Prooftoys is an effort to bring deeper and stronger understanding of
227mathematical proof to a wider audience, aided by computer
228implementation of principles of mathematical proof.
229
230The experience of two or more thousands of years of
231mathematical practice has shown that diverse minds from different
232backgrounds and different times can agree when a statement has been
233mathematically proven according to accepted principles, and when it
234has not.
235-->
236
237</section>
238
239      </div>
240      
241        
242          
243        
244      
245    </div>
246  
247
248
249<footer>
250  <a class="footer-logo" href="/">
251    <img src="/Logo1.svg">
252  </a>
253  <a href="/faq/">Q & A</a>
254  <a href="/news/">News</a>
255  <a href="/privacy/">Privacy</a>
256</footer>
257
258
259
260
261

262<script src="/popper.min.js">
263</script>

263

264<script src="/tippy-bundle.umd.js">
265</script>

265
266
267  
268  
269  
270  
271  
272  
273  
274  
275  
276  
277  
278  
279  
280  
281  
282  
283  
284  
285  
286     
287    

287<script src="/js/all.js"></script>

287
288  
289
290  
291

292<script type=module src="/js/db.js"></script>

292
293
294
295
296
297

298<script>
299
300
301
302if (Toy.TOC) {
303  $(Toy.TOC).tableofcontents({exclude: $('h1, .hero *, .sidebar *, h5, h6')});
304}
305Toy.mathifyAll();
306$(function() {
307  
308  
309  tippy('[data-tippy-content]', {
310    theme: 'light-border',
311    allowHTML: true,
312    
313    inlinePositioning: true,
314    
315    interactive: true,
316    
317    
318    appendTo: () => document.body,
319    
320    
321    delay: [400, 400],
322  });
323});
324
325
326$('#main').removeClass('invisible');
327</script>

327
328
329</body>
330
331</html>