Karteikarten
05 Logical Agents
Karten in diesem Stapel (18)
- 1What is a knowledge base and how can knowledge be gained?Set of sentences in a formal language coming from domain-specific content
-Inference (from domain-independent algorithms)
-Declarative (from outside)
-Perception (by agent) - 2What does logic consist of?-Syntax (correctness of sentence)
-Semantics (meaning)
-Model (evaluation of sentences to true or false)
-Satisfaction (sentence true in model)
-Entailment (relationship between two sentences, where truth of one requires truth of the other) - 3Which are the components of propositional logic?-Negation
-Conjunction
-Disjunction
-Implication
-Biconditional
=> Backus-Naur Form - 4Which inference rules are there?-Inference by enumeration
-Inference by theorem proving
-Inference by proof by resolution - 5How does Inference by enumeration work and what can be said about time & space complexity?Enumerate all models & check whether a (alpha) is true in every model, in which KB is true
-Time complexity: O(2^n)
Space complexity: O(n) (depth-first) - 6How does Theorem Proving work and when should it be applied?Applying rules of inference directly to sentences, no model required
If number of models large, but length of proof is short - 7Name concepts of Theorem Proving!-Logical equivalence
-Validity (valid sentences = tautologies)
-Satisfiability - 8Which inference rules can be applied to derive a proof? (Check formal descriptions)-Modus Ponens
-And-Elimination
-Commutativity
-Associativity
-De Morgan
-Distributivity
-Double-negation elimination
-Contraposition
-Implication elimination
-Biconditional elimination - 9What is special about Proof by Resolution inference?-Yields a complete inference algorithm when coupled with a complete search algorithm
-Only applies to disjunction of literals (=clauses) - 10Why is the limitation to clauses not a problem?Every propositional logic can be reformulated as a conjunction of clauses: Conjunctive Normal Form (CNF)
- 11Which principle do inference procedures based on resolution therefore use?Proof by contradiction:
-Conversion into CNF
-Resolution rule applied to resulting clauses: each pair that contains complementary literals is resolved to produce a new clause, which is added to the others
-Until no new clauses to be added or two clauses resolve to yield empty clause - 12What does the Ground Resolution Theorem state?If a set of clauses is unsatisfiable, then the resolution closure of those clauses contains the empty clause
- 13What is special about Horn clauses?No proof by resolution required, only requires Modus Ponens as an inference method
Propositional symbol or (conjunction of symbols)=>symbol - 14What are natural reasoning algorithms for Horn clauses?-Forward Chaining
-Backward Chaining - 15How can Forward Chaining be illustrated best?AND-OR graph:
-Links joined by an arc indicate conjunction: every link must be proven
-Links joined w/o an arc indicate a disjunction: only one link has to be proven - 16How does the procedure of AND-OR graphs look like?Fire any rule whose premises are satisfied in the KB, add its conclusion to the KB until the query is found
- 17WWork backwards from query q, check if q is known already or prove by backward chaining all premises of some rule concluding q
Avoid loops (check if new subgoal on goal stack) and repeated work (check if new subgoal already proven true or false) - 18What are the differences between Forward & Backward Chaining?-FC: data-driven, BC: goal-driven
-FC may do lots of irrelevant work, computational effort of BC can be much less than linear in time & space
Informationen
- Beschreibung
- Artificial Intelligence Karteikarten am 05 Logical Agents, erstellt von Timo Bierwirth am 22/02/2018.
- Erstellt von
- Timo Bierwirth
- Aufrufe
- 5
- Bewertung