Answer set programming

• Normal logic program clause : an expression of the form

  A <- B1, ... Bn , not C1 ,...Cm

  
  

  where A,B,C atomic formulas and n? >= 0

  • head : A
  • body B ... C
  • if m = 0, the clause is called definite
  • if n=m=0, the clause is called a fact, otherwise a rule
  • Ground clause : a clause without variabels
• normal logic program

  a set of normal program clauses
• definite logic progam 


  a logic program consisting of definite program clauses only
• First-order logic interpretation :

  • CL := A <- B1, .. Bn, not C1, ... not Cm

  is interpreted as :

  FOLI(CL) :=$\forall (B_1 \wedge ... \wedge B_n \wedge \neg C_1 \wedge ... \wedge \neg C_m \rightarrow A)$
• First-order logic interpretation FOLI(P) of a normal logic program P :

  FOLI(P) := {FOLI(CL) | CL in P}
• Herbrand universe of a language : the set of all ground terms of the language
• Herbrand base B of a language : the set of all ground atmoic formulas of the language
• Every normal logic program P possesses at lesat one minimal Herbrand model