1

I have to express some basic Prolog code in classical first order logic (FOL). In Prolog i use lists, together with member/2 and append/3 a lot. Could you give me some tips for writing clauses like the ones in the toy example below in FOL? The xs are intended as variables...

Family(Parents(marge, homer), Kids(bart, lisa, maggie))
Family(Parents(kirk, luann), Kids(milhouse))

Family(Parents(_, _), Kids(x1)) ^ Member(x2, x1) -> SomeKid(x2)
Family(Parents(x1, x2), Kids(x3)) ^ Append(x1, x2, x3, xresult) -> WholeFamily(xresult)

Expected output SomeKid(x) x = bart (and so on)
Expected output WholeFamily(x) x = marge, homer, bart, lisa, maggie and so on

I know i could do parent(bart, homer), parent(lisa, homer) and so on, but in my application I have to write predicates and functions that take lists of variable arity, where any list could contain functions (e.g. [Person(Name(bart), Age(12)), ..., Person(Name(lisa), Age(10))].

Thank you in advance!

/JCR

|improve this question
  • 1
    Totally unclear... In FOL there are no lists. – Mauro ALLEGRANZA Feb 17 at 13:20
  • To express Kids(bart, lisa, maggie) we need a unary predicate Kid(x) and add the "axiom" : Kid(bart) ∧ Kid(lisa) ∧ Kid(maggie). – Mauro ALLEGRANZA Feb 17 at 13:21
  • SomeKid(x2) can be ∃x Kid(x). Similar for Married(marge,homer) and Parent_of(x,y), from which Parent-of(marge,bart) and Parent_of(homer,bart). – Mauro ALLEGRANZA Feb 17 at 13:26
  • With it we can try to define the relationship of Belong_to_the_same_Family(x,y) : ∀x∀y [Married(x,y) ∨ ∃z ∃w (Parent_of(z,x) ∧ Parent_of(w,x) ...]. – Mauro ALLEGRANZA Feb 17 at 13:28
  • @MauroALLEGRANZA Thanks. What i was after is something like a variable-arity predicate. Married, for example, is usually arity 2, but one could think of marriages with three people and so on. And then functions which take a variable number of arguments. But, if I understand you correctly, this is not possible with classic FOL... – JCR Feb 17 at 18:43
0

Might this pass as classic FOL? Where the Member function gets items recursively...

List(a, end)
List(a, List(b, end))
List(a, List(b, List(c, end)))

x1 = List(x2, -) -> Member(x2, x1)
x1 = List(-, x1) ^ Member(x2, x1) -> Member(x2, x1)

|improve this answer
  • 1
    No, that doesn't work. In your second formula, the first "List" is a predicate symbol, but the second one must be a function symbol. You cannot use the same symbol for both in FOL. However, you can introduce list constructors, say "cons/2" and "nil/0", and then specify that List(nil) holds and that ∀x∀y (List(y) -> List(cons(x,y))) holds. (The Prolog [..|..] notation is just syntactic sugar for such list constructors.) – Uwe Mar 19 at 22:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.