See also:
As written in 1998:
forall message,t, r, x, y ( (signed(message,K) & derivable(t, message) & subject(t, x) & predicate(t, r) & object(t, y)) -> r(x,y) )
As implemented in ~2003:
{ [] acc:credential [ log:semantics :F ]. :F log:includes { :str acc:endorsement[acc:signature :sig; acc:key :k]}. :k crypto:verify ([is crypto:md5 of :str] :sig). :str log:parsedAsN3 :G } log:implies { :G acc:certSupportedBy :k }.
Why do we think this is better than/different from "failed" AI efforts?
Hypertext | Data/Logic | |
---|---|---|
pre-web constraint | all links go both ways | every question can be answered yes/no by an effective decision
procedure. Full understanding or bust*. |
Web simplification | most links work; some links break; back-links are an optional extra | Any party can check a proof once one is found, but some questions take a long time or forever to answer. Partial understanding. |
Web benefits | scalability: I can link from my private file to google/yahoo/cnn, without a link back from them | decentralized vocabulary development, ... increased expressivity? |
*as characatured by Lenat at KT2001.
cf. FOL in wikipedia
:lois :believes [ rdf:subject :clark; rdf:predicate rdf:type; rdf:object :Wimp ]. :clark = :superman. { ?O1 = ?O2. ?S ?P ?O1 } => { ?S ?P ?O2 }.and ask it to --think, then it will conclude that lois thinks that superman is a wimp too:
:lois :believes [ rdf:subject :clark, :superman; rdf:predicate rdf:type; rdf:object :Wimp ].
:lois :believes { :clark rdf:type :Wimp }. :clark = :superman. { ?S1 = ?S2. ?S1 ?P ?O } => { ?S2 ?P ?O }.and ask it to think, it won't find any new conclusions. The occurrence of :clark within { :clark rdf:type :Wimp } is quoted.
cf reification tests in 0.8 release, proof ontology...
{ this a log:Falsehood }
<>.log:semantics a log:Falsehood.
_:a rdf:type daml:Restriction . _:a daml:onProperty rdf:type . _:a daml:maxCardinalityQ 0 . _:a daml:hasClassQ _:b . _:b daml:oneOf _:c . _:c daml:first _:a . _:c daml:rest daml:nil .
cf From KL-ONE to OWL: Description Logics in the Ivory Tower and the Semantic Web by Peter F. Patel-Schneider
Suppose we drop the P \/ not(P) constraint from FOL?
In the world of metamathematics, the intuitionists are not at all exotic, despite the centrality of the PEDC (hence the PEM) to the ordinary sense of consistency. Their opponents do not scorn them as irrationalists but, if anything, pity them for the scruples that do not permit them to enjoy some "perfectly good" mathematics. Non-Contradiction and Excluded Middle in Peter Suber's Logical Systems course notes
We lose DeMorgan's laws and such, but it seems like it should work. It's a well-trodden path (see Isabelle.