logictools/predicate.html at master · priitj/logictools · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
<!DOCTYPE html>
<html lang="en">
<head itemscope>

<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">

<meta name="description" content="Simple propositional logic solvers: easy to hack and experiment with.">
<meta name="author" content="Tanel Tammet">
<meta name="keywords" content="logic, solvers, propositions, dpll, resolution, truth table">

<meta itemprop="itemtype" content="http://schema.org/SoftwareApplication">
<meta itemprop="name" content="Logictools">
<meta itemprop="description" content="Simple propositional logic solvers: easy to hack and experiment with.">
<meta itemprop="url" content="http://logictools.org">
<meta itemprop="operatingSystems" content="Linux, Windows">
<meta itemprop="softwareApplicationCategory" content="WebApplication">

<meta property="og:title" content="Logictools">
<meta property="og:url" content="http://logictools.org">
<meta property="og:site_name" content="Logictools">
<meta property="og:type" content="website">
<meta property="og:description" content="Simple propositional logic solvers: easy to hack and experiment with.">
<meta property="fb:admins" content="tanel.tammet">

<link rel="shortcut icon" href="logo.png">

<title>Logictools</title>
<!-- Bootstrap core CSS -->
<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.4/css/bootstrap.min.css">
<!-- Custom styles for this template -->
<link href="wdb.css" rel="stylesheet">
<script>
// google analytics
  (function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
  (i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o),
  m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m)
  })(window,document,'script','//www.google-analytics.com/analytics.js','ga');

  ga('create', 'UA-61132529-1', 'auto');
  ga('send', 'pageview');
</script>
</head>

<body>

<div id="fb-root"></div>

<div class="navbar navbar-inverse navbar-static-top" style="background-color: #333333;">
  <div class="container">
    <div class="navbar-header">
      <button type="button" class="navbar-toggle" data-toggle="collapse" data-target=".navbar-collapse">
        <span class="icon-bar"></span>
        <span class="icon-bar"></span>
        <span class="icon-bar"></span>
      </button>
      <a class="navbar-brand" href="index.html">Logictools</a>
    </div>
    <div class="navbar-collapse collapse">
      <ul class="nav navbar-nav">
        <li class="dummy"><a href="index.html">Solve</a></li>
        <li class="dummy"><a href="propositional.html">Propositional logic</a></li>
        <li class="active"><a href="predicate.html">Predicate logic</a></li>
        <li class="dummy"><a href="download.html">Download</a></li>
        <li class="dummy"><a href="about.html">About</a></li>
      </ul>
    </div><!--/.navbar-collapse -->
  </div>
</div>

<!-- content after titlebar -->


<!-- Main jumbotron for a primary marketing message or call to action -->
<div class="jumbotron" >
  <div class="container" style="text-align: left; padding-left: 45px;">
    <h1 class="jumbotron_title">Predicate logic</h1>
    <p class="jumbotron_caption">Solvers and utilities
    </p>

<div style="font-family: Arial, Helvetica, sans-serif;">
We plan to add educational solvers and tools for
<a href="http://en.wikipedia.org/wiki/First-order_logic">first order predicate logic</a> in the future.
<p></p>
Meanwhile we recommend these options for learning
<ul style="margin-top: 10px;">
<li><a href="http://lambda.ee/w/images/0/06/Geoffreasoningnotes.pdf">Automated
Theorem Proving Course Content</a> by Geoff Sutcliffe is probably the best introductory material</li>
<li><a href="http://www.cl.cam.ac.uk/~jrh13/atp/index.html">
Handbook of Practical Logic and Automated Reasoning</a> contains code examples in ML in addition
to an
<a href="http://www.cambridge.org/us/academic/subjects/computer-science/programming-languages-and-applied-logic/handbook-practical-logic-and-automated-reasoning?format=HB">
excellent text</a></li>
<li><a href="https://en.wikipedia.org/wiki/Handbook_of_Automated_Reasoning">Handbook of Automated_Reasoning</a>
for in-depth papers
(<a href="http://www.amazon.com/Handbook-Automated-Reasoning-Volume-Set/dp/0262182238/ref=pd_sim_sbs_b_1?ie=UTF8&refRID=124AQMPSV6ZW9N4J28EG">here on Amazon</a>). </li>
</ul>

and for experimenting with general-purpose
<a href="http://en.wikipedia.org/wiki/Automated_theorem_proving">predicate logic solvers</a>:

<ul style="margin-top: 10px;">
<li><a href="https://www.cs.unm.edu/~mccune/otter/">Otter</a>: a classic, easy-to-use prover by McCune</li>
<li><a href="http://www.cs.miami.edu/~tptp/">The TPTP Problem Library</a> for Automated Theorem Proving by
Geoff Sutcliffe and Christian Suttner.
</li>
<li><a href="http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP">Online solvers on TPTP</a></li>
<li><a href="http://www.cs.miami.edu/~tptp/CASC/">The CADE ATP System Competition</a></li>
</ul>

Several specialized categories of predicate logic solvers exist in addition to the
<a href="http://en.wikipedia.org/wiki/Automated_theorem_proving">general-purpose solvers</a>
mentioned above. Some of the categories are:
<p>
<ul>
<li><a href="https://en.wikipedia.org/wiki/Satisfiability_modulo_theories">SMT</a>
(satisfiability modulo theories) solvers used for
<a href="https://en.wikipedia.org/wiki/Formal_verification">formal verification</a> like
<a href="http://research.microsoft.com/en-us/projects/z3m/">Z3</a>
and
<a href="http://pvs.csl.sri.com/">PVS</a></li>
<li><a href="https://en.wikipedia.org/wiki/Answer_set_programming">Answer set</a> based solvers
like <a href="http://www.dlvsystem.com/">DLV</a> and
<a href="http://www.tcs.hut.fi/Software/smodels/">Smodels</a>, see
<a href="https://www.mat.unical.it/aspcomp2013">the competition</a></li>

<li><a href="https://en.wikipedia.org/wiki/Description_logic">Description logic</a>
solvers, see <a href="http://www.cs.man.ac.uk/~sattler/reasoners.html">the list of implementations</a></li>
<li><a href="https://en.wikipedia.org/wiki/Web_Ontology_Language">OWL</a>
(web ontology language) solvers used in the context of
<a href="https://en.wikipedia.org/wiki/Semantic_Web">semantic web</a>, see
<a href="http://www.w3.org/2001/sw/wiki/OWL/Implementations">the list of implementations</a></li>
</ul>

</div>


  </div>
</div>


<!-- footer -->

<div class="ofooter">
  <div class="col-md-12 container ifooter">
  </div>
</div>


<!-- at-end-scripts -->

<script>
// instead of jquery

function gid(x) { return document.getElementById(x); }

// reading a file
/*
function handleFileSelect(evt) {
  var files = evt.target.files;
  for (var i = 0, f; f = files[i]; i++) {
    var reader = new FileReader();
    reader.onload = (function(theFile) {
      return function(e) { gid('propinput').value=e.target.result; };
    })(f);
    reader.readAsText(f);
  }
}

gid('files').addEventListener('change', handleFileSelect, false);
*/
</script>
<!-- ui with bootstrap -->
<script src="http://ajax.googleapis.com/ajax/libs/jquery/1.11.1/jquery.min.js"></script>
<script src="http://maxcdn.bootstrapcdn.com/bootstrap/3.3.4/js/bootstrap.min.js"></script>
<!-- Solver code -->
<!--
<script src="proplog_ui.js"></script>
<script src="proplog_parse.js"></script>
<script src="proplog_convert.js"></script>
<script src="proplog_generate.js"></script>
<script src="proplog_dpll.js"></script>
<script src="proplog_olddpll.js"></script>
<script src="proplog_naivedpll.js"></script>
<script src="proplog_searchtable.js"></script>
<script src="proplog_naiveres.js"></script>
<script src="proplog_res.js"></script>
-->


</body>
</html>