🚀 go-pugleaf

In article <92276.202706COMTET@FRECP12.BITNET> <COMTET@FRECP12.BITNET> writes:
>Recently I had courses in languages such as Prolog and Lisp. The beginning of t
>he course was an attempt to describe comprehensively all logic languages. There
>are some terms that I didn't quite understand such as :

>Horner's clause ( or assertion)
>Could somebody give me either the meaning of those words or give me references

	A Horn clause is any rule, fact, or query.
	
	Rules have the form A :- B1, B2, ... Bn.
	Facts have the form A.
	Queries have the form ?- A.

	"Languages have tended to work with Horn clauses because Horn
clauses lead to efficient implementations" (Sethi).

Carl Walker
--
Carl Walker				"Hectic days ahead of us,
Bucknell University			 Rotten ones behind,
Lewisburg, PA				 Keeping plastics in our pockets,
cwalker@canopus.bucknell.edu (! tmc.edu) Children never mind." - K, S, & W

In article <1akmqnINNihd@coral.bucknell.edu> cwalker@canopus.bucknell.edu
 (carleton walker `93) writes:

   >A Horn clause is any rule, fact, or query.
   >Rules have the form A :- B1, B2, ... Bn.
   >Facts have the form A.
   >Queries have the form ?- A.

  "?- A"? What does this mean? Does it have something to do with
logic? Anyway, you left out the information needed for a truly
comprehensive understanding of logic languages. Horn clauses are so
named after Alfred Horn, who showed that theories axiomatizable using
Horn clauses are precisely those whose models are closed under
substructures and direct products. The significance of this fact is
immense, or at any rate not to be sneezed at.

In article <92276.202706COMTET@FRECP12.BITNET> COMTET@FRECP12.BITNET writes:
>Recently I had courses in languages such as Prolog and Lisp. The beginning of t
>he course was an attempt to describe comprehensively all logic languages. There
>are some terms that I didn't quite understand such as :
>logic of the first order

Explication simpliste: les propositions mathematiques sont codees par
des termes, exemple : qqsoit  X ilexiste Y telque  p(X,Y) ou non p(Y,X).
si les quantificateurs portent sur des symboles 'de base' on est au premier
ordre, si ils portent sur l'existence d'une fonction telle que gnagna, 
on est a un ordre superieur. 
Voir bouquin d'algebre universelle, genre Burris and Sankapannavar,
ou Gratzer, ou ....
>Horner's clause ( or assertion)

de HORN ! pas a confondre avec le schema de horner pour l'evaluation
des polynomes, ni l'accordeoniste minuscule.

>Could somebody give me either the meaning of those words or give me references
>about suchsubjects (books or articles)?

reference classique sur prolog: clocksin et mellish
Bouquin de R Lallement (sp ?) Logique, reduction et deduction, chez MASSON
Il y a plusieurs bouquins sur l' "automated reasoning" (ou deduction)
dont un des co-auteurs est z. manna, et qui sont facile a lire, et dont
le titre m'echappe. (cette phrase est une clause du premier ordre !)

M Billaud

-- 
Michel BILLAUD                 :  billaud@geocub.greco-prog.fr
Departement d'Informatique     :  phone W: 56.84.57.92  // 56.84.69.22
IUT "A", Universite Bordeaux I :  "Personne n'est exempt de dire des sottises.
33405 Talence  (FRANCE)        :   Le malheur est de les dire curieusement"

In article <1992Oct8.071027.9935@greco-prog.fr> billaud@geocub.UUCP (Michel BILLAUD) writes:
sorry for posting in french, my intention was to send a mail, but
i pressed the wrong key and the &$%$& rn doesnt want to cancel my
own postings!
M.
-- 
Michel BILLAUD                 :  billaud@geocub.greco-prog.fr
Departement d'Informatique     :  phone W: 56.84.57.92  // 56.84.69.22
IUT "A", Universite Bordeaux I :  "Personne n'est exempt de dire des sottises.
33405 Talence  (FRANCE)        :   Le malheur est de les dire curieusement"

In article <1992Oct8.071027.9935@greco-prog.fr> billaud@greco-prog.fr 
(Michel BILLAUD) writes:

   >Explication simpliste: les propositions mathematiques sont codees par
   >des termes, exemple : qqsoit  X ilexiste Y telque  p(X,Y) ou non p(Y,X).
   >si les quantificateurs portent sur des symboles 'de base' on est au premier
   >ordre, si ils portent sur l'existence d'une fonction telle que gnagna, 
   >on est a un ordre superieur. 

   An explanation such as this can cause considerable confusion, I believe,
even for somebody who knows French (which I don't). For how are we to
make sense, given this explanation, of statements such as those of axiomatic
set theory, which are said to be first order, but are nevertheless read
"for every function.." etc?

  So I suggest another explanation: the essential characteristic of
statements of first order logic is that they contain quantifiers only over
the "objects" in some "domain". This domain may contain anything,
including functions. We get higher order logic if we introduce quantifiers
over subsets of the domain, functions over the domain, etc.

  From this it may appear that the distinction is of little importance,
since instead of using higher order logic, one may use first order
logic simply by expanding the domain to contain the functions, etc,
that one is interested in. And indeed this is what is done in set
theory.

  In logic, the importance of the distinction emerges when we consider
the concepts of "truth in a model" and logical consequence in first
order logic and in second order logic. They are defined in quite
similar term, using more formal versions of my explanation of the
quantifiers above. However, logical consequence in first order logic
has a set of complete formal inference rules. This is not true of
second or higher order logic. Also, it is possible to uniquely
characterize infinite structures by second order axioms. This can
not be done using first order axioms.

  Note: what about e.g. logic with infinite disjunctions? Is this
first or higher order? There seems to be no standard usage. So when
"first order logic" is spoken of, it is usually assumed that ordinary
predicate logic is intended, as in my remarks above.