From: Dan Connolly <connolly@w3.org>

Date: Mon, 02 Apr 2001 16:22:24 -0500

Message-ID: <3AC8ED90.F808F690@w3.org>

To: pat hayes <phayes@ai.uwf.edu>

CC: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, kenb@ccs.neu.edu, www-rdf-logic@w3.org

Date: Mon, 02 Apr 2001 16:22:24 -0500

Message-ID: <3AC8ED90.F808F690@w3.org>

To: pat hayes <phayes@ai.uwf.edu>

CC: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, kenb@ccs.neu.edu, www-rdf-logic@w3.org

pat hayes wrote: > > >Ken may have pointed out a problem with the KIF axiomatization for > >DAML+OIL. > > Yes. The issue of finite models is a delicate one for KIF itself, in > fact. If KIF is taken to be a strict first-order language then there > is no way to guarantee, on semantic grounds, that all lists are > finite. Would you please elaborate on that? Are you just saying that the earlier KIF specs goofed, or are you saying that there's no way, in first order logic, to specify the set of finite lists? It sounds very much like a claim you made earlier that induction (over, say, natural numbers) isn't first order. I've been researching that claim for a while, and I found some pretty persuasive evidence to the contrary; it was pointed out to me that (a) natural induction is a theorem in set theory (b) set theory has been axiomatized, finitely, in first order logic so (c) natural induction has been axiomatized, finitely, in first order logic. I haven't found the whole argument written up in detail, but as to the interesting bit, (b): [[[ Computer Assisted Proofs in Set Theory Belinfante's interest in computer assisted theorem proving has mainly concentrated on obtaining proofs of theorems in set theory using the first-order logic resolution-style theorem prover Otter, a powerful automated reasoning program developed by William McCune at Argonne National Laboratories. Robert Boyer's idea of using Kurt Gödel's finite axiomatization of set theory is the basis for all Otter proofs of theorems in set theory. Art Quaife in his remarkable PhD thesis showed how to reduce the plethora of Skolem functions that had plagued earlier work, and listed several hundred theorems in set theory that he proved. Belinfante explored the use of Otter for more advanced topics in set theory, including theorems about certain standard functions in set theory, cross products, ordinal number theory, equipollence, the theory of finite sets, partial ordering, transitive closure, and so on. ]]] -- Computer Assisted Theorem Proving http://www.math.gatech.edu/~belinfan/research/autoreas/ "Boyer's idea" refers to: @misc{ boyer86set, author = "R. Boyer and E. Lusk and W. McCune and R. Overbeek and M. Stickel and L. Wos", title = "Set Theory in First-Order Logic: Clauses for G¨odel's Axioms", text = "R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos. Set Theory in First-Order Logic: Clauses for G¨odel's Axioms. Journal of Automated Reasoning, 2:287 -- 327, 1986.", year = "1986" } which I haven't found a copy of online yet. -- Dan Connolly, W3C http://www.w3.org/People/Connolly/Received on Monday, 2 April 2001 17:22:50 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:34 UTC
*