12/13

  • Databases: store massive amounts of persistent data efficiently

  • They are reliable and: provide safe access to multiple users

  • Database management systems (DBMSs): Software systems that store and manage databases

  • They use relational data model for storing data in tables: A database consist of a schema and a database instance

  • Database schema: A set of relation schemas π‘†π‘β„Ž = {π΄π‘π‘π‘œπ‘’π‘›π‘‘, π΅π‘Ÿπ‘Žπ‘›π‘β„Ž, πΆπ‘’π‘ π‘‘π‘œπ‘šπ‘’π‘Ÿ}

  • SQL is: a language for querying relational data

  • hoare state: : A variable look up that assigns a real number to each variable in the program and the free variables in πœ™ and πœ“

  • Resolution restriction: Only apply certain resolution steps

  • The unit restriction: At least one parent clause has only one literal

  • A resolution proof satisfies the unit restriction if: all its steps satisfy it

  • The positive restriction (P-restriction): At least one of the parent clauses in every resolution step only consists of positive literals

  • The negative restriction (N-restriction) is defined similarly; one parent consists of negative literals only

  • Linear resolution n for a set of clauses F: Resolves a sequence of clauses 𝐢0, 𝐢1, … , 𝐢n, 𝐢0 ∈ 𝐹 is the base clause and 𝐢𝑛 = β–‘, Every step applies resolution for πΆπ‘–βˆ’1 and a side clause π΅π‘–βˆ’1, The side clause π΅π‘–βˆ’1 is either, A clause from 𝐹, π΅π‘–βˆ’1 = 𝐢𝑗 for some 𝑗 < IResolution-complete: If any entailment proved by resolution without a restriction is also proved with the resolution

  • Linear resolution, P-restriction, and N-restriction are: resolution-complete

  • If a set of clauses is a contradiction: It has at least one positive clause and one negative clause

  • Unit resolution is: not resolution-complete

  • SLD (Selective Linear Definite clause) is a: resolution restriction that is used for logic programs and PROLOG

  • It applies two resolution restrictions: linear and negative restriction

  • SLD is: not resolution-complete

  • It is resolution-complete for Horn clauses

  • A Horn clause is a set of literals with: at most one positive literal

  • SLD and unit resolution are resolution-complete when : applied for Horn clauses

  • SLD is: linear resolution and also N-restriction

  • Fact: π‘€π‘œπ‘‘β„Žπ‘’π‘Ÿ (π‘†π‘Žπ‘Ÿπ‘Ž , πΈπ‘šπ‘šπ‘¦ )

  • Procedure: Parent (x,y): β€” Mother(x,y)

  • Goal: ? β€” Parent(y,Emmy)