Logic for computer science and artificial intelligence /
Logic and its components (propositional, first-order, non-classical) play a key role in Computer Science and Artificial Intelligence. While a large amount of information exists scattered throughout various media (books, journal articles, webpages, etc.), the diffuse nature of these sources is proble...
| Κύριος συγγραφέας: | |
|---|---|
| Μορφή: | Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
London :
ISTE ;
2011.
Hoboken, NJ : Wiley, 2011. |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
| LEADER | 10259nam a2200661 4500 | ||
|---|---|---|---|
| 001 | ocn828298951 | ||
| 003 | OCoLC | ||
| 005 | 20170124071509.8 | ||
| 006 | m o d | ||
| 007 | cr |n||||||||| | ||
| 008 | 130223s2011 enka ob 001 0 eng d | ||
| 040 | |a EBLCP |b eng |e pn |c EBLCP |d YDXCP |d DG1 |d N$T |d OCLCF |d UMI |d UKDOC |d DEBBG |d DEBSZ |d OCLCQ |d IDEBK |d E7B |d OCLCQ |d COO |d OCLCQ |d GrThAP | ||
| 019 | |a 842860157 |a 875001762 | ||
| 020 | |a 9781118604182 |q (electronic bk.) | ||
| 020 | |a 1118604180 |q (electronic bk.) | ||
| 020 | |a 9781118604205 |q (electronic bk.) | ||
| 020 | |a 1118604202 |q (electronic bk.) | ||
| 020 | |a 9781118604267 | ||
| 020 | |a 1118604261 | ||
| 020 | |a 1848213018 | ||
| 020 | |a 9781848213012 | ||
| 020 | |z 9781848213012 | ||
| 029 | 1 | |a AU@ |b 000055873634 | |
| 029 | 1 | |a CHNEW |b 000600347 | |
| 029 | 1 | |a DEBBG |b BV042032034 | |
| 029 | 1 | |a DEBSZ |b 414175018 | |
| 029 | 1 | |a DEBSZ |b 431338353 | |
| 029 | 1 | |a NZ1 |b 15915983 | |
| 029 | 1 | |a DEBBG |b BV043395466 | |
| 035 | |a (OCoLC)828298951 |z (OCoLC)842860157 |z (OCoLC)875001762 | ||
| 037 | |a CL0500000408 |b Safari Books Online | ||
| 050 | 4 | |a QA76.9.L63 |b C34 2011 | |
| 072 | 7 | |a COM |x 005030 |2 bisacsh | |
| 072 | 7 | |a COM |x 004000 |2 bisacsh | |
| 082 | 0 | 4 | |a 006.3 |2 23 |
| 049 | |a MAIN | ||
| 100 | 1 | |a Caferra, Ricardo, |d 1945- | |
| 245 | 1 | 0 | |a Logic for computer science and artificial intelligence / |c Ricardo Caferra. |
| 264 | 1 | |a London : |b ISTE ; |c 2011. | |
| 264 | 1 | |a Hoboken, NJ : |b Wiley, |c 2011. | |
| 300 | |a 1 online resource (537 pages) : |b illustrations | ||
| 336 | |a text |b txt |2 rdacontent | ||
| 337 | |a computer |b c |2 rdamedia | ||
| 338 | |a online resource |b cr |2 rdacarrier | ||
| 504 | |a Includes bibliographical references and index. | ||
| 505 | 0 | 0 | |g Chapter 1 |t Introduction |g 1 -- |g 1.1 |t Logic, foundations of computer science, and applications of logic to computer science |g 1 -- |g 1.2 |t On the utility of logic for computer engineers |g 3 -- |g Chapter 2 |t A Few Thoughts Before the Formalization |g 7 -- |g 2.1 |t What is logic? |g 7 -- |g 2.1.1 |t Logic and paradoxes |g 8 -- |g 2.1.2 |t Paradoxes and set theory |g 9 -- |g l2.1.2.1 |t The answer |g 10 -- |g 2.1.3 |t Paradoxes in arithmetic and set theory |g 13 -- |g 2.1.3.1 |t The halting problem |g 13 -- |g 2.1.4 |t On formalisms and well-known notions |g 15 -- |g 2.1.4.1 |t Some "well-known" notions that could turn out to be difficult to analyze |g 19 -- |g 2.1.5 |t Back to the definition of logic |g 23 -- |g 2.1.5.1 |t Some definitions of logic for all |g 24 -- |g 2.1.5.2 |t A few more technical definitions |g 24 -- |g 2.1.5.3 |t Theory and meta-theory (language and meta-language) |g 30 -- |g 2.1.6 |t A few thoughts about logic and computer science |g 30 -- |g 2.2 |t Some historic landmarks |g 32 -- |g Chapter 3 |t Propositional Logic |g 39 -- |g 3.1 |t Syntax and semantics |g 40 -- |g 3.1.1 |t Language and meta-language |g 43 -- |g 3.1.2 |t Transformation rules for cnf and dnf |g 49 -- |g 3.2 |t The method of semantic tableaux |g 54 -- |g 13.2.1 |t A slightly different formalism: signed tableaux |g 58 -- |g 3.3 |t Formal systems |g 64 -- |g 3.3.1 |t A capital notion: the notion of proof |g 64 -- |g 3.3.2 |t What do we learn from the way we do mathematics? |g 72 -- |g 3.4 |t A formal system for PL (PC) |g 78 -- |g 3.4.1 |t Some properties of formal systems |g 84 -- |g 3.4.2 |t Another formal system for PL (PC) |g 86 -- |g 3.4.3 |t Another formal system |g 86 -- |g 3.5 |t The method of Davis and Putnam |g 92 -- |g 3.5.1 |t The Davis-Putnam method and the SAT problem |g 95 -- |g 3.6 |t Semantic trees in PL |g 96 -- |g 3.7 |t The resolution method in PL |g 101 -- |g 3.8 |t Problems, strategies, and statements |g 109 -- |g 3.8.1 |t Strategies |g 110 -- |g 3.9 |t Horn clauses |g 113 -- |g 3.10 |t Algebraic point of view of propositional logic |g 114 -- |g Chapter 4 |t First-order Terms |g 121 -- |g 4.1 |t Matching and unification |g 121 -- |g 4.1.1 |t A motivation for searching for a matching algorithm |g 121 -- |g 4.1.2 |t A classification of trees |g 123 -- |g 4.2 |t First-order terms, substitutions, unification |g 125 -- |g Chapter 5 |t First-Order Logic (FOL) or Predicate Logic (PL1, PC1) |g 131 -- |g 5.1 |t Syntax |g 133 -- |g 5.2 |t Semantics |g 137 -- |g 5.2.1 |t The notions of truth and satisfaction |g 139 -- |g 5.2.2 |t A variant: multi-sorted structures |g 150 -- |g 5.2.2.1 |t Expressive power, sort reduction |g 150 -- |g 5.2.3 |t Theories and their models |g 152 -- |g 5.2.3.1 |t How can we reason in FOL? |g 153 -- |g 5.3 |t Semantic tableaux in FOL |g 154 -- |g 5.4 |t Unification in the method of semantic tableaux |g 166 -- |g 5.5 |t Toward a semi-decision procedure for FOL |g 169 -- |g 5.5.1 |t Prenex normal form |g 169 -- |g 5.5.1.1 |t Skolemization |g 174 -- |g 5.5.2 |t Skolem normal form |g 176 -- |g 5.6 |t Semantic trees in FOL |g 186 -- |g 5.6.1 |t Skolemization and clausal form |g 188 -- |g 5.7 |t The resolution method in FOL |g 190 -- |g 5.7.1 |t Variables must be renamed |g 201 -- |g 5.8 |t A decidable class: the monadic class |g 202 -- |g 5.8.1 |t Some decidable classes |g 205 -- |g 5.9 |t Limits: Gödel's (first) incompleteness theorem |g 206 -- |g Chapter 6 |t Foundations of Logic Programming |g 213 -- |g 6.1 |t Specifications and programming |g 213 -- |g 6.2 |t Toward a logic programming language |g 219 -- |g 6.3 |t Logic programming: examples |g 222 -- |g 6.3.1 |t Acting on the execution control: cut"/" |g 229 -- |g 6.3.1.1 |t Translation of imperative structures |g 231 -- |g 6.3.2 |t Negation as failure (NAF) |g 232 -- |g 6.3.2.1 |t Some remarks about the strategy used by LP and negation as failure |g 238 -- |g 6.3.2.2 |t Can we simply deduce instead of using NAF? |g 239 -- |g 6.4 |t Computability and Horn clauses |g 241 -- |g Chapter 7 |t Artificial Intelligence |g 245 -- |g 7.1 |t Intelligent systems: AI |g 245 -- |g 7.2 |t What approaches to study AI? |g 249 -- |g 7.3 |t Toward an operational definition of intelligence |g 249 -- |g 7.3.1 |t The imitation game proposed by Turing |g 250 -- |g 7.4 |t Can we identify human intelligence with mechanical intelligence? |g 251 -- |g 7.4.1 |t Chinese room argument |g 252 -- |g 7.5 |t Some history |g 254 -- |g 7.5.1 |t Prehistory |g 254 -- |g 7.5.2 |t History |g 255 -- |g 7.6 |t Some undisputed themes in AI |g 256 -- |g Chapter 8 |t Inference |g 259 -- |g 8.1 |t Deductive inference |g 260 -- |g 8.2 |t An important concept: clause subsumption |g 266 -- |g 8.2.1 |t An important problem |g 268 -- |g 8.3 |t Abduction |g 273 -- |g 8.3.1 |t Discovery of explanatory theories |g 274 -- |g 8.3.1.1 |t Required conditions |g 275 -- |g 8.4 |t Inductive inference |g 278 -- |g 8.4.1 |t Deductive inference |g 279 -- |g 8.4.2 |t Inductive inference |g 280 -- |g 8.4.3 |t Hempel's paradox (1945) |g 280 -- |g 8.5 |t Generalization: the generation of inductive hypotheses |g 284 -- |g 8.5.1 |t Generalization from examples and counter examples |g 288 -- |g Chapter 9 |t Problem Specification in Logical Languages |g 291 -- |g 9.1 |t Equality |g 291 -- |g 9.1.1 |t When is it used? |g 292 -- |g 9.1.2 |t Some questions about equality |g 292 -- |g 9.1.3 |t Why is equality needed? |g 293 -- |g 9.1.4 |t Whatis equality? |g 293 -- |g 9.1.5 |t How to reason with equality? |g 295 -- |g 9.1.6 |t Specification without equality |g 296 -- |g 9.1.7 |t Axiomatization of equality |g 297 -- |g 9.1.8 |t Adding the definition of = and using the resolution method |g 297 -- |g 9.1.9 |t By adding specialized rules to the method of semantic tableaux |g 299 -- |g 9.1.10 |t By adding specialized rules to resolution |g 300 -- |g 9.1.10.1 |t Paramodulation and demodulation |g 300 -- |g 9.2 |t Constraints |g 309 -- |g 9.3 |t Second Order Logic (SOL): a few notions |g 319 -- |g 9.3.1 |t Syntax and semantics |g 324 -- |g 9.3.1.1 |t Vocabulary |g 324 -- |g 9.3.1.2 |t Syntax |g 325 -- |g 9.3.1.3 |t Semantics |g 325 -- |g Chapter 10 |t Non-classical Logics |g 327 -- |g l0.l |t Many-valued logics |g 327 -- |g 10.1.1 |t How to reason with p-valued logics? |g 334 -- |g 10.1.1.1 |t Semantic tableaux for p-valued logics |g 334 -- |g 10.2 |t Inaccurate concepts: fuzzy logic |g 337 -- |g 10.2.1 |t Inference in FL |g 348 -- |g 10.2.1.1 |t Syntax |g 349 -- |g 10.2.1.2 |t Semantics |g 349 -- |g 10.2.2 |t Herbrand's method in FL |g 350 -- |g 10.2.2.1 |t Resolution andFL |g 351 -- |g 10.3 |t Modal logics |g 353 -- |g 10.3.1 |t Toward a semantics |g 355 -- |g 10.3.1.1 |t Syntax (language of modal logic) |g 357 -- |g 10.3.1.2 |t Semantics |g 358 -- |g 10.3.2 |t How to reason with modallogics? |g 360 -- |g 10.3.2.1 |t Formal systems approach |g 360 -- |g 10.3.2.2 |t Translation approach |g 361 -- |g 10.4 |t Some elements of temporal logic |g 371 -- |g 10.4.1 |t Temporal operators and semantics |g 374 -- |g 10.4.1.1 |t A famous argument |g 375 -- |g 10.4.2 |t A temporal logic |g 377 -- |g 10.4.3 |t How to reason with temporal logics? |g 378 -- |g 10.4.3.1 |t The method of semantic tableaux |g 379 -- |g 10.4.4 |t An example of a PL for linear and discrete time; PTL (or PLTL) |g 381 -- |g 10.4.4.1 |t Syntax |g 331 -- |g 10.4.4.2 |t Semantics |g 382 -- |g 10.4.4.3 |t Method of semantic tableaux for PLTL (direct method) |g 333 -- |g Chapter 11 |t Knowledge and Logic: Some Notions |g 385 -- |g 11.1 |t What is knowledge? |g 335 -- |g 11.2 |t Knowledge and modal logic |g 389 -- |g 11.2.1 |t Toward a formalization |g 389 -- |g 11.2.2 |t Syntax |g 339 -- |g 11.2.2.1 |t What expressive power? An example |g 389 -- |g 11.2.2.2 |t Semantics |g 339 -- |g 11.2.3 |t New modal operators |g 391 -- |g 11.2.3.1 |t Syntax (extension) |g 391 -- |g 11.2.3.2 |t Semantics (extension) |g 391 -- |g 11.2.4 |t Application examples |g 392 -- |g 11.2.4.1 |t Modeling the muddy children puzzle |g 392 -- |g 11.2.4.2 |t Corresponding Kripke worlds |g 392 -- |g 11.2.4.3 |t Properties of the (formalization chosen for the) knowledge |g 394 -- |g Chapter 12 |t Solutions to the Exercises |g 395. |
| 520 | |a Logic and its components (propositional, first-order, non-classical) play a key role in Computer Science and Artificial Intelligence. While a large amount of information exists scattered throughout various media (books, journal articles, webpages, etc.), the diffuse nature of these sources is problematic and logic as a topic benefits from a unified approach. Logic for Computer Science and Artificial Intelligence utilizes this format, surveying the tableaux, resolution, Davis and Putnam methods, logic programming, as well as for example unification and subsumption. For non-classical logics, the. | ||
| 588 | 0 | |a Print version record. | |
| 650 | 0 | |a Computer logic. | |
| 650 | 0 | |a Artificial intelligence. | |
| 650 | 7 | |a COMPUTERS |x Enterprise Applications |x Business Intelligence Tools. |2 bisacsh | |
| 650 | 7 | |a COMPUTERS |x Intelligence (AI) & Semantics. |2 bisacsh | |
| 650 | 7 | |a Artificial intelligence. |2 fast |0 (OCoLC)fst00817247 | |
| 650 | 7 | |a Computer logic. |2 fast |0 (OCoLC)fst00872265 | |
| 655 | 4 | |a Electronic books. | |
| 776 | 0 | 8 | |i Print version: |a Caferra, Ricardo. |t Logic for Computer Science and Artificial Intelligence. |d London : Wiley, ©2013 |z 9781848213012 |
| 856 | 4 | 0 | |u https://doi.org/10.1002/9781118604182 |z Full Text via HEAL-Link |
| 994 | |a 92 |b DG1 | ||
