¸íÁ¦³í¸®
(Propositional Calculus)
ÀΰøÁö´É-Áö´ÉÇü ¿¡ÀÌÀüÆ®¸¦ Áß½ÉÀ¸·Î : Nils J.Nilsson Àú¼, ÃÖÁß¹Î. ±èÁØÅÂ. ½É±¤¼·. À庴Ź °ø¿ª, »çÀÌÅØ¹Ìµð¾î, 2000 (¿ø¼ : Artificial Intelligence : A New Synthesis 1998), Page 229~242
1. Ư¡°ª¿¡ ´ëÇÑ Á¦¾àÁ¶°ÇÀÇ »ç¿ë
¿ì¸®´Â ¾Õ¿¡¼ ¿¡ÀÌÀüÆ® ¼¼°è¸¦ ¸ðµ¨¸µÇÏ´Â µÎ °¡Áö ¼·Î ´Ù¸¥ ¹æ¹ýÀ¸·Î ¾ÆÀÌÄÜ (icon) À» ±â¹ÝÀ¸·Î ÇÑ °Í°ú Ư¡ (feature) À» ±â¹ÝÀ¸·Î ÇÑ °Í¿¡ ´ëÇØ »ìÆìº¸¾Ò´Ù. ÀÌÁø°ªÀ» °®´Â Ư¡µéÀº ¸ðµ¨¸µÇÏ´Â ¼¼°è¿¡¼ ¹«¾ùÀÌ »ç½ÇÀÌ°í ¹«¾ùÀÌ »ç½ÇÀÌ ¾Æ´ÑÁö¿¡ ´ëÇÑ ¹¦»ç (description) ÀÌ´Ù. ¾ÆÀÌÄܱâ¹Ý Ç¥Çö ¹æ½ÄÀº ±× ¼¼°èÀÇ Æ¯Á¤ Ãø¸é¿¡ ´ëÇÑ ½Ã¹Ä·¹ÀÌ¼Ç (simulation) ÀÌ´Ù. ´ë°³ÀÇ °æ¿ì, ½Ã¹Ä·¹À̼ÇÀÌ ¹¦»çº¸´Ù Á÷Á¢ÀûÀ̰í È¿°úÀûÀ̱ä ÇÏÁö¸¸ ¹¦»çµµ ³ª¸§´ë·ÎÀÇ ÀåÁ¡ÀÌ ÀÖ´Ù. ¿¡ÀÌÀüÆ® »çÀÌÀÇ Åë½ÅÀÇ °æ¿ì, Ư¡°ªµéÀº ´Ù¸¥ ¿¡ÀÌÀüÆ®¿¡°Ô Àü´ÞµÇ±â ½¬¿î ¹Ý¸é, ¾ÆÀÌÄÜ ¸ðµ¨Àº µ¶¸³ÀûÀÎ Á¶°¢µé·Î ³ª´©¾î Á¡ÁøÀûÀÎ (incremental) Åë½ÅÀ» ÇϱⰡ ¾î·Æ´Ù. ¶ÇÇÑ Æ¯Â¡°ªÀ» °è»êÇÏ´Â µ¥¿¡ ÇÊ¿äÇÑ ÀÎÁö °úÁ¤Àº ¾ÆÀÌÄÜ ¸ðµ¨À» ¸¸µé°Å³ª ¼öÁ¤ÇÏ´Â °Íº¸´Ù ÈξÀ °£´ÜÇÏ´Ù. ±×¸®°í ¾î¶² Ư¼ºµéÀÇ °ªÀ» Á÷Á¢ ÀνÄÇϱ⠾î·Á¿î °æ¿ì, ¿¡ÀÌÀüÆ®°¡ ¼ÓÇÑ ¼¼°è¿¡ ÀÖ´Â Á¦¾àÁ¶°ÇµéÀ» ÀÌ¿ëÇÏ¿© ´Ù¸¥ Ư¡°ªµé·ÎºÎÅÍ ±× °ªÀ» Ãß·ÐÇÒ ¼öµµ ÀÖ´Ù.
»Ó¸¸ ¾Æ´Ï¶ó, ¿¡ÀÌÀüÆ® ȯ°æÀÇ ¾î¶² Á¤º¸¿¡ ´ëÇØ¼´Â ¾ÆÀÌÄÜÈÇÏ¿© Ç¥ÇöÇϱⰡ ¾î·Æ°Å³ª ºÒ°¡´ÉÇÑ °æ¿ì°¡ ÀÖ´Ù. ´ÙÀ½ÀÇ ¿¹¸¦ º¸ÀÚ.
ÀÌ¿Í °°ÀÌ Ç¥ÇöÇϱ⠾î·Á¿î Á¤º¸ÀÇ ÀϺδ Ư¡°ª¿¡ ´ëÇÑ Á¦¾àÁ¶°Ç (constraints) À¸·Î °ø½Ä鵃 ¼ö ÀÖ´Ù. ¿¡ÀÌÀüÆ®°¡ Á¸ÀçÇÏ´Â ¼¼°è¿¡ ´ëÇÑ Áß¿äÇÑ Áö½ÄÀ» Ç¥ÇöÇÏ´Â Á¦¾àÁ¶°ÇµéÀº Á÷Á¢ ÀÎ½ÄµÉ ¼ö ¾ø´Â Ư¡°ªµéÀ» Ãß·ÐÇϴµ¥ ¸¹ÀÌ ÀÌ¿ëµÈ´Ù (Ư¡µé »çÀÌÀÇ Á¦¾àÁ¶°Ç¿¡ ±â¹ÝÀ» µÐ °è»êÀ» ¼öÇàÇÏ¿©). ¿¡ÀÌÀüÆ®ÀÇ ÇöÀç »óÅ¿¡ ´ëÇÑ Á¤º¸¸¦ ÃßÃøÇÏ´Â °ÍÀº (ÀÌ Ã¥ÀÇ 2 ºÎ¿¡ ¼³¸íÇÑ Å½»ö ¹æ¹ýµéÀ» ÀÌ¿ëÇÏ¿©) ¿¡ÀÌÀüÆ®ÀÇ ÇൿÀÇ °á°ú·Î ³ªÅ¸³ª´Â ¹Ì·¡ »óŸ¦ °è»êÇÏ´Â °Í°ú ´ëÁ¶µÈ´Ù. óÀ½ ÇàÀ§¸¦ Ãß·Ð (reasoning), ³ªÁß °ÍÀ» Åõ¿µ (projecting) À̶ó°í Çϸç, ´ÙÀ½ ¸î °³ Àå¿¡¼´Â Åõ¿µ ¹®Á¦´Â Á¢¾î µÎ°í Ã߷п¡ ´ëÇØ ÁýÁßÀûÀ¸·Î ´Ù·ê °ÍÀÌ´Ù.
Ư¡°ªÀ» Ãß·ÐÇÏ´Â °Í°ú °ü·ÃµÈ ¸î °¡Áö ÀÀ¿ë ºÐ¾ß°¡ ÀÖ´Ù. ¹«¾ùº¸´Ù Ãß·ÐÀº ¿¡ÀÌÀüÆ®°¡ ÇൿÀ» °áÁ¤ÇÒ ¶§ ¿¡ÀÌÀüÆ®ÀÇ È¿À²¼ºÀ» ³ô¿© ÁØ´Ù (¹ÝÀÀÇü ¿¡ÀÌÀüÆ®ÀÎ °æ¿ì¿¡µµ). ´Ù¸¥ ÀÀ¿ë ºÐ¾ßµµ ¸¹ÀÌ Àִµ¥ ¿¹¸¦ µé¾î, »ý¹°À̳ª ÀüÀÚ ±â°è ½Ã½ºÅÛ µîÀÇ ¹°¸®ÀûÀÎ ½Ã½ºÅÛÀÇ ±â´ÉÀ» ÀûÀýÇÑ Æ¯Â¡ÀÇ ÁýÇÕÀ¸·Î Ç¥½ÃÇÒ ¼ö ÀÖ´Ù´Â °ÍÀÌ ¾Ë·ÁÁ® ÀÖÀ¸¸ç, ÀÌ Æ¯Â¡µé »çÀÌÀÇ Á¦¾àÁ¶°ÇµéÀº Á¶Á÷À̳ª ÀåÄ¡¿¡ °üÇÑ ¹°¸®Àû ȤÀº ±× ¹ÛÀÇ ±ÔÄ¢À» ³ªÅ¸³½´Ù. ÀÌ·± °æ¿ì Ãß·ÐÀº ½Ã½ºÅÛÀÇ Àå¾Ö¸¦ Áø´ÜÇÏ´Â µîÀÇ ¸ñÀûÀ¸·Î »ç¿ëµÉ ¼ö ÀÖ´Ù. ¿¹¸¦ µé¾î, "¿øÀÎ" °ú °ü·ÃµÈ Ư¡µéÀ» "Áõ»ó" °ú °ü·ÃµÈ Ư¡µé·ÎºÎÅÍ Ãß·ÐÇÒ ¼ö ÀÖ´Ù. ÀÌ¿Í °°Àº ÀϹÝÀûÀÎ Á¢±Ù ¹æ½ÄÀº AI ÀÇ Áß¿äÇÑ ÀÀ¿ë ºÐ¾ßÀÇ ÇϳªÀÎ Àü¹®°¡ ½Ã½ºÅÛ¿¡ ¸Å¿ì Áß¿äÇÏ´Ù.
Ãß·Ð ¹æ¹ýµéÀ» ¼³¸íÇϱ⿡ ¾Õ¼ µ¿±â¸¦ ºÎ¿©ÇÒ ¸¸ÇÑ ¿¹Á¦¸¦ Çϳª »ìÆìº¸ÀÚ. ºí·ÏÀÌ ³Ê¹« ¹«°ÌÁö ¾Ê°í, ·Îº¿ÀÇ ¹èÅ͸® ÆÄ¿ö ¼Ò½º°¡ ÀûÀýÇÏ¸é ºí·ÏÀ» µé ¼ö ÀÖ´Â ·Îº¿À» »ý°¢ÇØ º¸ÀÚ. ¸¸ÀÏ ÀÌ µÎ °¡Áö Á¶°ÇÀÌ ¸¸Á·µÈ´Ù¸é ·Îº¿ÀÌ ÀÚ½ÅÀÌ Àâ°í ÀÖ´Â ºí·ÏÀ» µé·Á°í ÇÒ ¶§ ÆÈÀÌ ¿òÁ÷ÀÏ °ÍÀÌ´Ù. ¿ì¸®´Â ÀÌ ¿©·¯ °¡Áö Á¶°ÇµéÀ» ÀÌÁø°ªÀ» °®´Â Ư¡µé·Î ´ÙÀ½°ú °°ÀÌ Ç¥ÇöÇÒ ¼ö ÀÖ´Ù.
(BAT_OK)
(LIFTABLE)
(MOVES)
¼³¸íÀ» µ½±â À§ÇØ °ýÈ£ ¾ÈÀÇ Æ¯Â¡À» ±â¾ïÇϱ⠽¬¿î À̸§µé·Î Áö¾ú´Ù. ·Îº¿ÀÌ °è±â¸¦ Àоî BAT_OK ¸¦, Á¶ÀÎÆ® °¢µµ ¼¾¼¸¦ ÀÌ¿ëÇÏ¿© MOVES ¸¦ °¨ÁöÇÒ ¼ö ÀÖ°í LIFTABLE Àº ¾Ë ¼ö ¾ø´Ù°í °¡Á¤ÇÏÀÚ. ±×·¯³ª LIFTABLE ÀÇ °ªÀº ·Îº¿ÀÌ ¼öÇàÇØ¾ß ÇÏ´Â ÀÏÀ» °áÁ¤ÇÏ´Â µ¥ ¸Å¿ì Áß¿äÇÏ´Ù. ¿ì¸®ÀÇ ¿¹Á¦¿¡¼´Â BAT_OK ¿Í LIFTABLE ÀÇ °ªÀÌ 1 ÀÏ ¶§ MOVES µµ 1 ÀÌ´Ù. ¸¸ÀÏ ·Îº¿ÀÌ ¿òÁ÷ÀÌ·Á ½ÃµµÇßÀ» ¶§, MOVES °¡ 0 À̶ó¸é BAT_OK À̳ª LIFTABLE ÀÇ °ª Áß Çϳª´Â 0 À̾î¾ß ÇÑ´Ù. BAT_OK °ªÀÌ 1 ·Î °¨ÁöµÇ¾ú´Ù¸é LIFTABLE ÀÇ °ªÀÌ 0 À̾î¾ß ÇÑ´Ù. ¿ì¸®°¡ ÀÌ¿Í °°ÀÌ Ãß·ÐÇÒ ¼ö ÀÖÀ¸¹Ç·Î, ·Îº¿µµ ÀÌ·¸°Ô ÇÒ ¼ö ÀÖµµ·Ï ÇØº¸ÀÚ. À̸¦ À§ÇØ Æ¯Â¡ »çÀÌÀÇ Á¦¾àÁ¶°Ç°ú Ư¡°ªÀ» Ç¥ÇöÇÒ ¼ö ÀÖ´Â ¾ð¾î (language) ¿Í ÇÊ¿äÇÑ Ãß·ÐÀ» ¼öÇàÇÒ ¼ö ÀÖ´Â Ãß·Ð ¹æ¹ý (inference mechanism) ÀÌ ÇÊ¿äÇÏ´Ù. ºÎ¿ï ´ë¼ö¿¡¼ ÆÄ»ýµÈ ¸íÁ¦³í¸® (propositional calculus) °¡ ÀÌ·¯ÇÑ ÇÊ¿äÇÑ µµ±¸µéÀ» Á¦°øÇÑ´Ù.
À§ ¿¹Á¦ÀÇ Á¦¾àÁ¶°ÇÀº ¸íÁ¦³í¸® ¾ð¾î·Î ´ÙÀ½°ú °°ÀÌ ³ªÅ¸³¾ ¼ö ÀÖ´Ù.
BAT_OK ¡ü LIFTABLE ¡ù MOVES
¿©±â¼ ¡ü ´Â ±×¸®°í (and) ¸¦, ¡ù ´Â ÇÔÀÇÇÏ´Ù (implies) ¸¦ ÀǹÌÇÑ´Ù.
ÀÌ ¾ð¾î¿¡´Â ÁÖ¾îÁø ¹®ÀåÀ¸·ÎºÎÅÍ °á·ÐÀ» À¯µµÇÏ´Â µ¥ ÀÌ¿ëÇÒ ¼ö ÀÖ´Â ±â¹ýµéÀÌ ÀÖ´Ù. ÀΰøÁö´É¿¡¼´Â ³í¸®¾ð¾îµéÀÌ ¸Å¿ì Áß¿äÇϹǷΠÀÌ ¾ð¾îµéÀ» ±â¹ÝÀ¸·Î ÇÏ´Â ´õ º¹ÀâÇϰí Áö´ÉÀûÀÎ ¿¡ÀÌÀüÆ®¸¦ ¼Ò°³Çϱâ Àü¿¡ ÀÌ ±â¹ýµé¿¡ ´ëÇØ ÀÚ¼¼È÷ ´Ù·ê °ÍÀÌ´Ù.
¿ì¼± ¸î °¡Áö Á¤Àǰ¡ ÀÖ´Ù. ³í¸® (logic) ´Â ´ÙÀ½À» Æ÷ÇÔÇÑ´Ù.
¿©±â¼´Â µÎ °¡Áö ³í¸®¾ð¾î¿¡ ´ëÇÏ¿© ¼Ò°³ÇÒ °ÍÀÌ´Ù. ù ¹øÂ°´Â µÎ °¡Áö Áß »ó´ëÀûÀ¸·Î °£´ÜÇÑ ¸íÁ¦³í¸® (propositional calculus) À̰í, µÎ ¹øÂ°´Â ´õ À¯¿ëÇÏ°Ô ÀÌ¿ëµÇ´Â ÀÏÂ÷ ¼ú¾î³í¸® (first-order predicate calculus, FOPC) ÀÌ´Ù. ÀÏÂ÷ ¼ú¾î³í¸®¿¡¼ÀÇ Áß¿äÇÑ ¸¹Àº °³³äµéÀÌ ¸íÁ¦³í¸®¿¡¼ º¸´Ù °£´ÜÇÏ°Ô ¼³¸íµÉ ¼ö ÀÖÀ¸¹Ç·Î ¸íÁ¦³í¸®¸¦ ¿ì¼± ¼Ò°³ÇϰڴÙ.
¸íÁ¦³í¸®ÀÇ ¿ä¼ÒµéÀ» ü°èÀûÀ¸·Î ¼³¸íÇϰڴÙ. ¿ì¼±Àº ÀÌ ¾ð¾îÀÇ ¿ä¼ÒµéÀ» ÀÇ¹Ì¿Í °áºÎ½ÃŰÁö ¾Ê´Â °ÍÀÌ ÁÁ´Ù. Áö±ÝºÎÅÍ ¿ì¸®°¡ ÇÏ´Â ÀÏÀ» ÀÇ¹Ì ¾ø´Â °ÔÀÓÀÇ ±ÔÄ¢À» ¼³¸íÇÏ´Â °ÍÀ¸·Î »ý°¢ÇÏÀÚ. Àǹ̿¡ ´ëÇØ¼´Â ³ªÁß¿¡ À̾߱âÇÒ °ÍÀÌ´Ù. ÀÌ ¾ð¾îÀÇ ¿ä¼ÒµéÀº ´ÙÀ½°ú °°´Ù.
¾ÆÅè (atoms) : µÎ ¾ÆÅè T ¿Í F ±×¸®°í P, Q, R, ..., P1, P2, ON_A_B µî°ú °°ÀÌ ´ë¹®ÀÚ·Î ½ÃÀÛÇÏ´Â ¹®ÀÚ¿ÀÇ ¹«ÇÑ ´ë ÁýÇÕ.
¿¬°áÀÚ (connectives) : "¶Ç´Â (or)", "±×¸®°í (and)", "ÇÔÀÇ (implies)", "ºÎÁ¤ (not)" À» °¢°¢ ³ªÅ¸³»´Â ¡ý, ¡ü, ¡ù, ¡þ (³ªÁß¿¡ ÀÌ ¿¬°áÀÚµéÀÇ Àǹ̸¦ À̸§°ú °ü·ÃÇØ ¼³¸íÇϰڴÙ. Áö±ÝÀº ±×³É Àǹ̰¡ ¾ø´Â ±âÈ£µéÀ̶ó°í ÇÏÀÚ).
¹®Àå (sentences) À̶ó°íµµ ÇÏ´Â Á¤Çü½Ä (well-formed formulas, wffs) ÀÇ ¹®¹ý :
¾ÆÅèµéÀº wff ÀÌ´Ù.
¤ý¿¹ : P, R, P3
°ú
°¡ wff ÀÌ¸é ´ÙÀ½µµ wff ÀÌ´Ù.
¤ý ¡ý
(
°ú
ÀÇ ³í¸®ÇÕ (disjunction))
¡ü
(
°ú
ÀÇ ³í¸®°ö (conjunction))
¡ù
(ÇÔÀÇ (implication))
¡þ (
ÀÇ ºÎÁ¤ (negation))
¾ÆÅè°ú ¡þ °¡ ºÙ¾î ÀÖ´Â ¾ÆÅèµéÀ» ¸®ÅÍ·² (literal)
À̶ó°í ÇÑ´Ù. ¡ù
¿¡¼
Àº ÇÔÀÇÀÇ ÀüÁ¦ (antecedent) ¶ó°í Çϰí
´Â °á·Ð (consequent) À̶ó°í ÇÑ´Ù.
wff ÀÇ ¿¹ :
(P ¡ü Q) ¡ù ¡þP
P ¡ù ¡þP
P ¡ý P ¡ù P
(P ¡ù Q) ¡ù (¡þQ ¡ù ¡þP)
¡þ¡þP
¤ý±× ÀÌ¿ÜÀÇ wff ´Â ¾ø´Ù.
¿¹ : P ¡ù ¡þ¡þ´Â wff °¡ ¾Æ´Ï´Ù.
¾ÕÀÇ ¿¹Á¦¿¡¼ ÀÌ¿ëµÈ ±¸º°ÀÚ '(' ¿Í ')' ´Â wff µéÀ» ¹¾î ´Ù½Ã wff ¸¦ ¸¸µå´Â ¿ªÇÒÀ» ÇÑ´Ù. ³í¸®¸¦ ´Ù·ê ¶§ ±¸º°ÀÚ¸¦ ¾ð¾îÀÇ ÀϺηΠ°ø½ÄÈÇÏ¿© ´Ù·ç´Â °æ¿ìµµ ÀÖÀ¸³ª, ¿©±â¼´Â ±×·¸°Ô±îÁö ¾ö°ÝÇÏ°Ô Á¤ÀÇÇÏ¿© »ç¿ëÇÏÁö´Â ¾Ê°Ú´Ù. ¾î¶² ¹®ÀåÀÌ wff ÀÎÁö´Â wff ÀÇ Á¤ÀǸ¦ Àç±ÍÀûÀ¸·Î Àû¿ëÇÏ¿© ÆÇ´ÜÇÒ ¼ö ÀÖ´Ù. ¿¹¸¦ µé¾î, (P ¡ü Q) ¡ù ¡þR ÀÌ wff ÀÓÀ» º¸ÀÌÀÚ. ¿ì¼±, P ¿Í Q °¡ wff À̹ǷΠ(P ¡ü Q) µµ wff ÀÌ´Ù. ¶ÇÇÑ R ÀÌ wff À̹ǷΠ¡þR µµ wff ÀÌ´Ù. ±×·¯¹Ç·Î (P ¡ü Q) ¡ù ¡þR Àº wff ÀÌ´Ù.
wff µé·ÎºÎÅÍ ´Ù¸¥ wff µéÀ» ¸¸µå´Â ¹æ¹ýÀº ¿©·¯
°¡Áö°¡ Àִµ¥, À̵éÀ» Ãß·Ð ±ÔÄ¢ (rules of inference) À̶ó°í ÇÑ´Ù. Ãß·Ð ±ÔÄ¢Àº
º¸Åë ´Â ¥á ·ÎºÎÅÍ (ȤÀº ¥á ¿Í ¥â ·ÎºÎÅÍ) Ãß·ÐµÉ ¼ö ÀÖ´Ù´Â ½ÄÀÇ ÇüŸ¦ °¡Áö°í
ÀÖ´Ù. ´ÙÀ½Àº ÈçÈ÷ ÀÌ¿ëµÇ´Â Ãß·Ð ±ÔÄ¢µéÀÌ´Ù.
wff ÀÇ ¼øÂ÷ ÁýÇÕ (sequence) À» wff ÀÇ ÁýÇÕ ¥Ä ·ÎºÎÅÍÀÇ
ÀÇ Áõ¸í (proof) (ȤÀº ¿¬¿ª (deduction)) À̶ó°í ÇÏ´Â °ÍÀº, ¼øÂ÷ ÁýÇÕ¿¡ ÀÖ´Â
°¢
°¡ ¥Ä ¿¡ Á¸ÀçÇϰųª ¶Ç´Â ¼øÂ÷ ÁýÇÕ¿¡¼
º¸´Ù ¾Õ¿¡ ³ª¿À´Â wff µé·ÎºÎÅÍ
°¡ Ãß·Ð ±ÔÄ¢À» ÀÌ¿ëÇÏ¿© Ãß·ÐµÉ ¼ö ÀÖ´Ù´Â °ÍÀ» ÀǹÌÇÑ´Ù. ¥Ä ·ÎºÎÅÍ
ÀÌ Áõ¸íµÉ ¼ö ÀÖ´Ù´Â °ÍÀ» ´ÙÀ½°ú °°ÀÌ Ç¥±âÇÑ´Ù.
Áõ¸í°ú Á¤¸®ÀÇ °³³äÀº »ç¿ëµÇ´Â Ãß·Ð ±ÔÄ¢ÀÇ ÁýÇÕ°ú
°ü·ÃÀÌ ÀÖ´Ù. Ãß·Ð ±ÔÄ¢ÀÇ ÁýÇÕÀ» ¹®ÀÚ ·Î Ç¥±âÇϸé,
¿¡ ÀÖ´Â Ãß·Ð ±ÔÄ¢À» ÀÌ¿ëÇÏ¿© ¥Ä ·ÎºÎÅÍ
ÀÌ Áõ¸íµÉ ¼ö ÀÖ´Ù´Â °ÍÀ» ´ÙÀ½°ú °°ÀÌ Ç¥±âÇÑ´Ù.
¿¹ : wff ÀÇ ÁýÇÕ {P, R, P ¡ù Q} °¡ ÁÖ¾îÁ³À» ¶§, ´ÙÀ½ÀÇ ¼øÂ÷ ÁýÇÕÀº ¾Õ¿¡ ¼Ò°³µÈ Ãß·Ð ±ÔÄ¢µé¿¡ ÀÇÇØ Q ¡ü R ÀÇ Áõ¸íÀÌ µÈ´Ù.
{P, P ¡ù Q, Q, R, Q ¡ü R}
Áõ¸íÀÇ °³³äÀº ¼øÂ÷ ÁýÇÕ»Ó ¾Æ´Ï¶ó ºÎºÐ ¼ø¼ (partial order) ·Îµµ ¼³¸íÇÒ ¼ö ÀÖ´Ù. ºÎºÐ ¼ø¼´Â Æ®¸® ±¸Á¶·Î Ç¥½ÃµÉ ¼ö ÀÖ´Ù. Áõ¸íÆ®¸® (proof tree) ÀÇ °¢ ³ëµå´Â wff °¡ µÇ¸ç, ¹Ýµå½Ã ¥Ä ¿¡ ÀÖ´Â wff À̰ųª Æ®¸®ÀÇ ºÎ¸ð ³ëµåµé·ÎºÎÅÍ Ãß·Ð ±ÔÄ¢À» ÀÌ¿ëÇÏ¿© Ãß·ÐµÉ ¼ö ÀÖ´Â °ÍÀ̾î¾ß ÇÑ´Ù. ÀÌ Æ®¸®°¡ ·çÆ® ³ëµå¿¡ ´ëÇÑ Áõ¸íÀÌ´Ù. ±×¸² 1 ¿¡ Áõ¸íÆ®¸®ÀÇ ¿¹°¡ ÀÖ´Ù.
ÀÌÁ¦ ÀÇ¹Ì (meanings) ¿¡ ´ëÇØ ³íÀÇÇØ º¸ÀÚ. Àǹ̷Р(semantics) Àº ³í¸®¾ð¾îÀÇ ¿ä¼ÒµéÀ» Ç¥ÇöÇϰíÀÚ ÇÏ´Â ¹®Á¦ ¿µ¿ªÀÇ ¿ä¼Ò¿Í ¿¬°ü½ÃŰ´Â °ÍÀÌ´Ù. ÀÌ ¿¬°üÀÌ ¹Ù·Î ¿ì¸®°¡ ¸»ÇÏ´Â ÀÇ¹Ì (meanings) ÀÌ´Ù. ¸íÁ¦³í¸®ÀÇ °æ¿ì, ¾ÆÅèÀ» ½Ç¼¼°è¿¡ ´ëÇÑ ¸íÁ¦ (proposition) ¿¡ ¿¬°ü½ÃŲ´Ù (±×·¡¼ À̸§ÀÌ ¸íÁ¦³í¸®ÀÌ´Ù). ¿¹¸¦ µé¾î ¾ÆÅè BAT_OK ¸¦ ¹èÅ͸®°¡ ÃæÀüµÇ¾ú´Ù¶ó´Â ¸íÁ¦¿¡ ¿¬°ü½Ãų ¼ö ÀÖ´Ù (¾ÆÅèÀÇ À̸§ÀÌ ¹Ýµå½Ã ±â¾ïÇϱ⠽¬¿î ¹®ÀÚ¿ÀÏ ÇÊ¿ä´Â ¾ø´Ù. À̸§À» ´Ù¸£°Ô ÁöÀ» ¼öµµ ÀÖ´Ù). ¾ÆÅèÀ» ¸íÁ¦¿¡ ¿¬°ü½ÃŰ´Â °ÍÀ» ÇØ¼® (interpretation) À̶ó°í ÇÑ´Ù. ÁÖ¾îÁø ÇØ¼®¿¡¼ ¾ÆÅè°ú ¿¬°üµÈ ¸íÁ¦¸¦ ±× ¾ÆÅèÀÇ ÀÇ¹Ì (denotation) ¶ó°í ÇÑ´Ù.
ÁÖ¾îÁø ÇØ¼®ÇÏ¿¡¼ ¾ÆÅèÀº ±× °ªÀ¸·Î True ȤÀº False ¸¦ °®´Â´Ù. ¸¸ÀÏ ¾ÆÅè ¥á °¡ ¸íÁ¦ P ¿Í ¿¬°üµÇ¾ú´Ù¸é ¥á ´Â P °¡ ½Ç¼¼°è¿¡ ´ëÇØ Áø½ÇÀÎ °æ¿ì¿¡ True °ªÀ» °¡Áö¸ç, ±×·¸Áö ¾ÊÀº °æ¿ì¿¡´Â False °ªÀ» °®´Â´Ù. ¾ÆÅè T ´Â Ç×»ó True, ¾ÆÅè F ´Â Ç×»ó False °ªÀ» °®´Â Ưº°ÇÑ ¾ÆÅèÀÌ´Ù. ½Ç¼¼°è¿¡ ´ëÇÑ ¸íÁ¦µéÀº ÀÌ»óÀûÀ¸·Î´Â Ç×»ó Áø½Ç ¾Æ´Ï¸é °ÅÁþÀ̹ǷΠ°¢ ¾ÆÅèÀÌ ½Ç¼¼°è¿¡ ´ëÇÑ ¾î¶² ¸íÁ¦¸¦ Áö½ÃÇÏ´Â °ÍÀÎÁö¿¡ °ü°è¾øÀÌ ¾ÆÅè¿¡ Á÷Á¢ °ªÀ» ÇÒ´çÇÒ ¼ö ÀÖ´Ù.
¸¸ÀÏ ½Ç¼¼°è¿¡ ´ëÇÑ ¸íÁ¦ÀÇ ÁøÀ§ ¿©ºÎ¸¦ °¡¸®´Â
µ¥ ÀÌ¿ëµÉ ¿¡ÀÌÀüÆ®ÀÇ °¨Áö ÀåÄ¡°¡ ½Å·ÚÇÒ ¼ö ÀÖ´Â °ÍÀ̶ó¸é, °¨ÁöµÈ Ư¡ ÀÇ °ªÀÌ 1 ÀÏ ¶§ ÇØ´çÇÏ´Â ¸íÁ¦´Â ÂüÀÏ °ÍÀÌ¸ç ¿¬°üµÈ ¸íÁ¦³í¸® ¾ÆÅè (X1 À̶ó
ÇÏÀÚ) Àº True °ªÀ» °¡Áú °ÍÀÌ´Ù. ±×·¸±â ¶§¹®¿¡, °¨ÁöµÈ Á¤º¸¸¦ ÀԷ¼±ÀÇ 1 °ú 0
°ªÀ¸·Î Ç¥½ÃÇÏ´Â ´ë½Å¿¡, ±× Á¤º¸¸¦ Áö½Äº£À̽º (knowledge base) ¶ó°í ÇÏ´Â ¿¡ÀÌÀüÆ®ÀÇ
¸Þ¸ð¸® ±¸Á¶¿¡ ¸íÁ¦³í¸® ¾ÆÅèÀ¸·Î Ç¥ÇöÇÒ ¼ö ÀÖ´Ù. ¿¡ÀÌÀüÆ®ÀÇ Áö½Äº£À̽º¿¡ X1 °ú
°°Àº ¾ÆÅèÀÌ ³ªÅ¸³´Ù´Â °ÍÀº ¿¡ÀÌÀüÆ®°¡ ±× ¾ÆÅè¿¡ ¿¬°üµÈ ¸íÁ¦°¡ ½Ç¼¼°è¿¡¼ »ç½ÇÀ̶ó°í
»ý°¢ÇÑ´Ù´Â °ÍÀ» ÀǹÌÇÑ´Ù. ¿¡ÀÌÀüÆ®°¡ ÀÚ½ÅÀÇ Áö½Äº£À̽º¿¡¼ wff µéÀ» ¾î¶»°Ô ÀÌ¿ëÇÏ´ÂÁö
°ð »ìÆìº¼ °ÍÀÌ´Ù.
¾î¶² ÇØ¼®ÇÏ¿¡¼ ¾ÆÅèµéÀÇ °ªÀÌ ÁÖ¾îÁ³À» ¶§, Áø¸®Ç¥
(truth table) ¸¦ ÀÌ¿ëÇÏ¸é °°Àº ÇØ¼®ÇÏ¿¡¼ ÀÓÀÇÀÇ wff ¿¡ ´ëÇÑ °ªÀ» °è»êÇÒ ¼ö
ÀÖ´Ù. Áø¸®Ç¥´Â ¿¬°áÀÚµéÀÇ Àǹ̸¦ Á¤¸³ÇÑ´Ù. °ú
¸¦ wff ¶ó°í Çϸé Áø¸®Ç¥ÀÇ ±ÔÄ¢Àº ´ÙÀ½°ú °°´Ù.
Ç¥ 1 ¸íÁ¦ Áø¸®Ç¥
|
|
|
|
|
|
True |
True |
True |
True |
False |
True |
True |
False |
False |
True |
False |
False |
False |
True |
False |
True |
True |
True |
False |
False |
False |
False |
True |
True |
À§ÀÇ ±ÔÄ¢µéÀº º¸Åë Ç¥ 1 °ú °°ÀÌ Ç¥ÀÇ Çü½ÄÀ¸·Î ³ªÅ¸³»¹Ç·Î À̵éÀ» Áø¸®Ç¥ ±ÔÄ¢À̶ó°í ºÎ¸¥´Ù.
wff ÀÇ ±¸¼º ¾ÆÅèÀÇ °ªÀÌ ÁÖ¾îÁö¸é Áø¸®Ç¥¸¦ ÀÌ¿ëÇÏ¿© ¾î¶² wff ÀÇ °ªµµ ±¸ÇÒ ¼ö ÀÖ´Ù. Áø¸®Ç¥¸¦ ÀÌ¿ëÇÏ¿© wff ÀÇ °ªÀ» ±¸ÇÏ´Â ¿¹¸¦ µé¾îº¸ÀÚ. P ´Â False, Q µµ False, R Àº True ¶ó°í °¡Á¤Çϸé [(P ¡ù Q) ¡ù R] ¡ù P ÀÇ Áø¸® °ªÀº ¹«¾ùÀΰ¡? ¾ÈÂÊ¿¡¼ºÎÅÍ °è»êÇÏ¸é ¿ì¼± P ¡ù Q ´Â True À̰í (P ¡ù Q) ¡ù R µµ True °¡ µÈ´Ù. ¸¶Áö¸·À¸·Î P °¡ False À̹ǷΠÀüü ½ÄÀº False °¡ µÈ´Ù.
¸¸ÀÏ ¿¡ÀÌÀüÆ®°¡ ÀÚ½ÅÀÌ ¼ÓÇÑ ¼¼°è¸¦ (¸íÁ¦¿¡ ÇØ´çÇÏ´Â) n °³ÀÇ Æ¯Â¡À¸·Î ³ªÅ¸³»°í, ÀÌ Æ¯Â¡µéÀ» ¿¡ÀÌÀüÆ®ÀÇ ¸ðµ¨¿¡¼ °¢°¢¿¡ ÇØ´çÇÏ´Â n °³ÀÇ ¾ÆÅèÀ¸·Î ³ªÅ¸³¾ ¼ö ÀÖ´Ù¸é, n °³ÀÇ ¾ÆÅèÀÌ °¢°¢ True ¾Æ´Ï¸é False °ªÀ» °®´Â °æ¿ìÀÇ ¼ö°¡ 2©ú À̹ǷΠ¿¡ÀÌÀüÆ®°¡ ÀνÄÇÏ´Â ¼¼°è´Â 2©ú °¡ÁöÀÇ ´Ù¸¥ »óȲÀÌ ÀÖÀ» ¼ö ÀÖ´Ù. ÀÌ·¯ÇÑ ¿¡ÀÌÀüÆ® ¼¼°èÀÇ °¢°¢ÀÇ »óȲÀÌ ÇØ¼® (interpretation) ¿¡ ÇØ´çÇÑ´Ù. n °³ÀÇ ¾ÆÅèÀÇ °ªµé (ÇØ¼®) ÀÌ ÁÖ¾îÁö¸é, ¿¡ÀÌÀüÆ®´Â Áø¸®Ç¥¸¦ ÀÌ¿ëÇÏ¿© ¾î¶² wff ÀÇ °ªµµ ±¸ÇÒ ¼ö ÀÖ´Ù. ¹Ý´ëÀÇ ÇÁ·Î¼¼½ºµµ °¡´ÉÇѰ¡? wff ÀÇ ÁýÇÕ¿¡¼ wff µéÀÇ °ªÀÌ ÁÖ¾îÁ³´Ù°í °¡Á¤ÇÏÀÚ. ÀÌ °ªµé·ÎºÎÅÍ À¯ÀÏÇÑ ÇØ¼®ÀÌ À¯µµµÉ ¼ö Àִ°¡? Á¾Á¾ ¿¡ÀÌÀüÆ®¿¡°Ô´Â (True °ªÀ» °®´Â wff µé·Î Ç¥ÇöµÈ) Ư¡µé¿¡ ´ëÇÑ Á¦¾àÁ¶°Çµé¸¸ ÁÖ¾îÁö±â ¶§¹®¿¡ ÀÌ Áú¹®Àº Áß¿äÇÑ Àǹ̸¦ °®´Â´Ù. ±×·¯¸é ¿¡ÀÌÀüÆ®´Â ¾ÆÅèµéÀÇ °ªÀ» À¯µµÇÒ ¼ö ÀÖ°í µû¶ó¼ ½Ç¼¼°è¿¡ ´ëÇÑ ÇØ´ç ¸íÁ¦°¡ ÂüÀÎÁö °ÅÁþÀÎÁö ÆÇº°ÇÒ ¼ö ÀÖÀ»±î? Áï, ÁÖ¾îÁø ½ÄµéÀÌ ½Ç¼¼°èÀÇ 2©ú °¡Áö °¡´ÉÇÑ »óȲ Áß Çϳª¸¦ ÁöÁ¤Çϴ°¡? ´äÀº º¸Åë "¾Æ´Ï¿À" ÀÌ´Ù. ´ë½Å wff ÁýÇÕÀÇ ¸ðµç wff ¸¦ True ·Î ÇÏ´Â ÇØ¼®Àº ¿©·¯ °³ ãÀ» ¼ö ÀÖ´Ù. ÀÌ ÁÖÁ¦¸¦ ´Ù·ç±â À§ÇØ ¸ðµ¨À̶ó´Â ¿ë¾î¸¦ ´ÙÀ½ Àý¿¡¼ ¼Ò°³ÇÑ´Ù.
wff °¡ ÁÖ¾îÁø ÇØ¼® ¾Æ·¡ True À̸é ÇØ¼®Àº ±× wff ¸¦ ¸¸Á·½ÃŲ´Ù (satisfy) °í ÇÑ´Ù. wff ¸¦ ¸¸Á·½ÃŰ´Â ÇØ¼®À» ±× wff ÀÇ ¸ðµ¨ (model) À̶ó°í Çϸç wff ÁýÇÕÀÇ °¢ wff ¸¦ ¸ðµÎ ¸¸Á·½ÃŰ´Â ÇØ¼®À» ±× wff ÁýÇÕÀÇ ¸ðµ¨À̶ó°í ÇÑ´Ù. ÇØ¼®Àº °¢ ¾ÆÅè¿¡ °ªÀ» ÇÒ´çÇÏ´Â °ÍÀ̹ǷΠ¿ì¸®´Â ÇØ¼®ÀÌ ¾ÆÅèÀ» ¸¸Á·½ÃŰ´ÂÁö ½±°Ô ¾Ë ¼ö ÀÖ´Ù. ±×¸®°í ³ª¼ Áø¸®Ç¥¸¦ ÀÌ¿ëÇÏ¿© ÇØ¼®ÀÌ ¾ÆÅèµé·Î ÀÌ·ç¾îÁø wff ¸¦ ¸¸Á·½ÃŰ´ÂÁö ¾Ë ¼ö ÀÖ´Ù.
¾Õ¿¡¼ ¸»ÇÑ ºí·ÏÀ» µé¾î¿Ã¸®´Â ·Îº¿¿¡¼ Ư¡µé¿¡ ´ëÇÑ Á¦¾àÁ¶°ÇÀº ´ÙÀ½ wff ·Î Ç¥ÇöµÇ¾ú´Ù.
BAT_OK ¡ü LIFTABLE ¡ù MOVES
À§ÀÇ wff °¡ True °ªÀ» °®´Â´Ù¸é BAT_OK ¿Í LIFTABLE ÀÌ True À̰í MOVES °¡ False ÀÎ °æ¿ì´Â ¹èÁ¦µÇ¾î¾ß ÇÑ´Ù. °¢ Á¦¾àÁ¶°ÇÀÇ wff ´Â °¡´ÉÇÑ ¸ðµ¨ Áß¿¡ ¹èÁ¦µÇ¾î¾ß ÇÒ °ÍµéÀ» ¾Ë·ÁÁØ´Ù (°¢ ¸ðµ¨Àº ½Ç¼¼°è°¡ óÇÒ ¼ö ÀÖ´Â ¿©·¯ °¡Áö »óȲ ÁßÀÇ Çϳª¸¦ ³ªÅ¸³½´Ù). ÀϹÝÀûÀ¸·Î ¼¼°è¸¦ ³ªÅ¸³»´Â wff ÀÇ ¼ö°¡ ¸¹À»¼ö·Ï ¸ðµ¨ÀÇ ¼ö´Â Àû¾îÁø´Ù. ½Ç¼¼°è¿¡ ´ëÇØ ¾Æ´Â °ÍÀÌ ´õ ¸¹¾ÆÁö¸é ½Ç¼¼°è°¡ óÇÒ ¼ö ÀÖ´Â »óȲ¿¡ ´ëÇÑ ºÒÈ®½Ç¼ºÀÌ ÁÙ¾îµå´Â °ÍÀÌ ´ç¿¬ÇÏ´Ù.
wff (ȤÀº wff ÁýÇÕ) ¸¦ ¸¸Á·½ÃŰ´Â ÇØ¼®ÀÌ ¾øÀ» ¼öµµ ÀÖ´Ù. ÀÌ·± °æ¿ì, ±× wff (ȤÀº wff ÁýÇÕ) ¸¦ ¸ð¼øÀÌÀÖ´Ù (inconsistent) ȤÀº ¸¸Á·½Ãų ¼ö ¾ø´Ù (unsatisfiable) °í ¸»ÇÑ´Ù. ¸¸Á·½Ãų ¼ö ¾ø´Â wff ÀÇ ¿¹·Î´Â F ¿Í P ¡ü¡þP µîÀÌ ÀÖ´Ù (¾î¶² ÇØ¼®µµ À̵é wff ¸¦ ¸¸Á·½Ãų ¼ö ¾ø´Ù). ¸¸Á·½Ãų ¼ö ¾ø´Â wff ÁýÇÕÀÇ ´Ù¸¥ ¿¹´Â {P ¡ý Q, P ¡ý ¡þQ, ¡þP ¡ý Q, ¡þP ¡ý ¡þQ} ÀÌ´Ù (Áø¸®Ç¥¸¦ ÀÌ¿ëÇÏ¿© ¾î¶² ÇØ¼®µµ ¸ðµç wff ¸¦ True ·Î ¸¸µé ¼ö ¾øÀ½À» È®ÀÎÇ϶ó).
wff °¡ ±¸¼ºÇÏ´Â ¾ÆÅèÀÇ ¸ðµç ÇØ¼®¿¡ ´ëÇØ True À̸é Ÿ´ç (valid) ÇÏ´Ù°í ÇÑ´Ù (Ÿ´çÇÑ wff ´Â ½Ç¼¼°è¿¡ ´ëÇÑ ¾Æ¹«·± Á¤º¸µµ ÁÖÁö ¾ÊÀ¸¹Ç·Î ¹«ÀǹÌÇÏ´Ù). ´ÙÀ½Àº Ÿ´çÇÑ wff ÀÇ ¿¹ÀÌ´Ù.
Áø¸®Ç¥¸¦ ÀÌ¿ëÇÏ¿© wff ÀÇ Å¸´ç¼ºÀ» Áõ¸íÇÏ·Á¸é ¾ÆÅè°ªÀÇ ¸ðµç Á¶ÇÕ¿¡ ´ëÇØ µûÁ®º¸¾Æ¾ß ÇϹǷΠ¾ÆÅè ¼ö¿¡ Áö¼öÀûÀ¸·Î ºñ·ÊÇÏ´Â ½Ã°£ÀÌ °É¸°´Ù.
µÎ wff ÀÇ Áø¸®°ªÀÌ ¸ðµç ÇØ¼®¿¡ ´ëÇØ °°À» ¶§ ±× µÎ wff µéÀº µ¿Ä¡ (equivalence) ¶ó°í ¸»ÇÏ°í ¡Õ ±âÈ£·Î ³ªÅ¸³½´Ù. Áø¸®Ç¥¸¦ ÀÌ¿ëÇÏ¿© ´ÙÀ½ µ¿Ä¡ °ü°è¸¦ Áõ¸íÇÒ ¼ö ÀÖ´Ù.
wff °¡ ÁýÇÕ ¥Ä ¿¡ ÀÖ´Â ¸ðµç wff ¸¦ True ·Î ÇÏ´Â ÇØ¼®¿¡ ´ëÇØ True °ªÀ» °¡Áö¸é
¥Ä ´Â
¸¦ ³í¸®ÀûÀ¸·Î ±Í°áÇÑ´Ù (logically entails) °í Çϸç
´Â ¥Ä ¸¦ ³í¸®ÀûÀ¸·Î µû¸¥´Ù (logically follows) °í ÇÑ´Ù. ±×¸®°í
´Â ¥Ä ÀÇ ³í¸®Àû °á·Ð (logical consequence) À̶ó°í ÇÑ´Ù. ³í¸®Àû ±Í°áÀº ±âÈ£
¸¦ ÀÌ¿ëÇÏ¿©
·Î Ç¥½ÃÇÑ´Ù.
¸¶Áö¸· µÎ ¿¹¿¡¼´Â ¥Ä °¡ ´ÜÀÏ ¾ÆÅèÀ¸·Î ÀÌ·ç¾îÁø °æ¿ì ÈçÈ÷ ÇÏ´Â ´ë·Î ÁýÇÕ ±âÈ£¸¦ »ý·«ÇÏ¿´´Ù.
³í¸®Àû ±Í°áÀº ¾î¶² ¸íÁ¦µéÀÌ »ç½ÇÀÏ ¶§ °ü½ÉÀÌ ÀÖ´Â ´Ù¸¥ ¸íÁ¦ (Á÷Á¢ °¨ÁöµÉ ¼ö ¾ø´Â) ÀÇ »ç½Ç ¿©ºÎµµ ¾Ë·ÁÁÖ´Â ¹æ¹ýÀ» Á¦°øÇϹǷΠÀΰøÁö´É ºÐ¾ß¿¡¼ ¸Å¿ì Áß¿äÇÑ °³³äÀÌ´Ù. ¿¹¸¦ µé¾î, ½Ç¼¼°è¿¡ ´ëÇÑ ¿ì¸®ÀÇ Áö½ÄÀ» BAT_OK ¡ü LIFTABLE ¡ù MOVES ½ÄÀ¸·Î Ç¥ÇöÇϰí, BAT_OK ¹× ¡þMOVES ¿Í °ü·ÃµÈ Ư¡À» °¨ÁöÇÑ´Ù°í °¡Á¤ÇØ º¸ÀÚ. Áï 3 °³ÀÇ ½ÄÀÌ Àִµ¥ µÎ °³´Â ½Ç¼¼°èÀÇ Æ¯Á¤ÇÑ »óȲÀ» ³ªÅ¸³»´Â °ÍÀÌ°í ³ª¸ÓÁö Çϳª´Â ½Ç¼¼°è¿¡ ´ëÇÑ ÀϹÝÀûÀÎ Áö½ÄÀ» ³ªÅ¸³»´Â °ÍÀÌ´Ù. ¡þLIFTABLE ÀÌ ÀÌµé ¼¼ °³ÀÇ ½Ä¿¡ ÀÇÇØ ³í¸®ÀûÀ¸·Î ±Í°áµÈ´Ù´Â °ÍÀ» Áø¸®Ç¥¸¦ ÀÌ¿ëÇÏ¿© °¢ÀÚ È®ÀÎÇØ º¸±â ¹Ù¶õ´Ù. ÀÌ·¯ÇÑ ±Í°á¿¡ µû¶ó, ¡þLIFTABLE Àº ¼¼ °³ ½ÄÀ» ¸ðµÎ True °¡ µÇ°Ô ÇÏ´Â ¸ðµç ÇØ¼®¿¡ ´ëÇØ True À̰í, µû¶ó¼ ¿ì¸®°¡ ÀǵµÇÏ´Â ÇØ¼® (LIFTABLE ¿¡ ´ëÇÑ ·Îº¿ ¼¼°è¿Í °ü·ÃµÈ ÇØ¼®) ¿¡ ´ëÇØ¼ True À̾î¾ß ÇÑ´Ù. ±×·¯¹Ç·Î ¿ì¸®ÀÇ ÀǵµµÈ ÇØ¼®ÀÎ "ºí·ÏÀº µé ¼ö ¾ø´Ù" ¶ó´Â ¸íÁ¦´Â True À̾î¾ß ÇÏ´Â °ÍÀÌ´Ù!
±Í°áÀº ½Ç¼¼°è¿¡ ´ëÇÑ ¸íÁ¦ÀÇ ÁøÀ§ ¿©ºÎ¸¦ °áÁ¤ÇÏ´Â µ¥ ¸Å¿ì °·ÂÇÑ µµ±¸°¡ µÇ¹Ç·Î Á¤º¸¸¦ wff ·Î Ç¥ÇöÇϰí È¿°úÀûÀ¸·Î ´Ù¸¥ wff µéÀ» ±Í°áÇÏ´Â ¹æ¹ýÀ» ¿¬±¸ÇÏ´Â °ÍÀº ¸Å¿ì Áß¿äÇÏ´Ù. Áø¸®Ç¥¸¦ ÀÌ¿ëÇÏ¿© Ç×»ó ÀÌ·± ÀÛ¾÷À» ¼öÇàÇÒ ¼ö ÀÖÁö¸¸, ´õ °£´ÜÇÑ ¹æ¹ýÀÌ ÀÖ´Ù. ±Í°á (entailment) ´ë½Å »ç¿ëÇÒ ¼ö ÀÖ´Â ÇϳªÀÇ ¸Å·ÂÀûÀÎ ¹æ¹ýÀº Ãß·Ð (inference) ÀÌ´Ù. À̵éÀº ±Ùº»ÀûÀ¸·Î´Â ´Ù¸¥ °³³äÀÌÁö¸¸, Á¤´ç¼º (soundness) °ú ¿ÏÀü¼º (completeness) ¿¡ ÀÇÇØ ¼·Î ¿¬°üµÈ´Ù.
Ãß·ÐÀ» ±Í°á°ú ¿¬°üÁþ´Â µÎ °¡Áö Á¤ÀÇ´Â ´ÙÀ½°ú °°´Ù (ÀÌÁ¦ Á¤¸® (theorem) ¿Í Áõ¸í (proof), µÎ ´Ü¾îÀÇ Á÷°üÀûÀÎ Àǹ̸¦ ¼³¸íÇÑ´Ù).
1. ÀÓÀÇÀÇ wff ÁýÇÕ ¥Ä ¿Í wff ¿¡ ´ëÇØ,
°¡
¸¦ ÇÔÀÇÇϸé (implies), ±× Ãß·Ð ±ÔÄ¢ÀÇ ÁýÇÕ
À» Á¤´çÇÏ´Ù (sound) °í ÇÑ´Ù.
2. ÀÓÀÇÀÇ wff ÁýÇÕ ¥Ä ¿Í wff ¿¡ ´ëÇØ,
ÀÏ ¶§, Ãß·Ð ±ÔÄ¢ÀÇ ÁýÇÕ
À» ÀÌ¿ëÇÏ¿© ¥Ä ·ÎºÎÅÍ
ÀÇ Áõ¸íÀÌ Á¸ÀçÇÑ´Ù¸é,
Àº ¿ÏÀüÇÏ´Ù (complete) °í ÇÑ´Ù.
¾ÆÁ÷ ¸íÁ¦ ³í¸®¸¦ À§ÇÑ ¿ÏÀüÇÑ Ãß·Ð ±ÔÄ¢ÀÇ ÁýÇÕ¿¡ ´ëÇÏ¿©´Â À̾߱âÇÏÁö ¾Ê¾ÒÀ¸¸ç, ¿©±â¿¡ ´ëÇØ¼´Â ´ÙÀ½ Àå¿¡¼ ´Ù·ê °ÍÀÌ´Ù.
Ãß·Ð ±ÔÄ¢ÀÌ Á¤´çÇÏ°í ¿ÏÀüÇϸé Áø¸®Ç¥¸¦ ÀÌ¿ëÇÏÁö ¾Ê°íµµ Áõ¸íÀ» Ž»öÇÔÀ¸·Î½á ÇÑ wff °¡ wff ÁýÇÕÀ» ³í¸®ÀûÀ¸·Î µû¸£´ÂÁö ¾Æ´ÑÁö °áÁ¤ÇÒ ¼ö ÀÖ´Ù.
Ãß·Ð ±ÔÄ¢ÀÌ Á¤´çÇÑ °æ¿ì, ¥Ä ·ÎºÎÅÍ ÀÇ Áõ¸íÀ» ã¾Æ³»¸é
°¡ ¥Ä ¸¦ ³í¸®ÀûÀ¸·Î µû¸£´Â °ÍÀÌ´Ù. Ãß·Ð ±ÔÄ¢ÀÌ ¿ÏÀüÇÑ °æ¿ì, Áõ¸íÀ» ã±â
À§ÇÑ Å½»ö ¹æ¹ýÀ» ÀÌ¿ëÇÏ¿©
°¡ ¥Ä ¸¦ ³í¸®ÀûÀ¸·Î µû¸£´ÂÁö¸¦ ±Ã±ØÀûÀ¸·Î È®ÀÎÇÒ ¼ö ÀÖ´Ù. Áø¸®Ç¥¸¦ ´ë½ÅÇÏ¿©
Áõ¸í ¹æ¹ýÀ» ÀÌ¿ëÇÏ´Â °ÍÀº ¸íÁ¦³í¸®³ª ¼ú¾î³í¸® ¸ðµÎ¿¡¼ °è»êÀûÀ¸·Î Å©°Ô À¯¸®ÇÏ´Ù
(¿©±â¿¡ ´ëÇØ¼´Â ³ªÁß¿¡ ´Ù·ê °ÍÀÌ´Ù).
ÇϳªÀÇ wff °¡ ¾î¶² wff ÁýÇÕÀ» ³í¸®ÀûÀ¸·Î µû¸£´ÂÁö, ¶Ç´Â ¾î¶² wff ÁýÇÕÀ¸·ÎºÎÅÍ Áõ¸íµÉ ¼ö ÀÖ´ÂÁö °áÁ¤ÇÏ´Â ¹®Á¦´Â ÀϹÝÀûÀ¸·Î NP-hard ¹®Á¦ÀÌ´Ù [Cook 1971] (Áï, º¹Àâµµ°¡ ¾ÆÅè ¼ö¿¡ Áö¼öÀûÀ¸·Î ºñ·ÊÇÏ´Â °Íº¸´Ù ÀÛ´Ù°í Áõ¸íµÉ ¼ö ¾ø´Â ¹®Á¦ÀÌ´Ù). ±×·³¿¡µµ ºÒ±¸Çϰí, °è»ê °¡´ÉÇÑ Æ¯¼öÇÑ °æ¿ìµéÀÌ ÀÖÀ¸¹Ç·Î ³í¸®ÀûÀÎ Ãß·Ð °úÁ¤À» ÀÌÇØÇÏ´Â °ÍÀº Áß¿äÇÑ °ÍÀÌ´Ù.
´ë°³ÀÇ °æ¿ì ¿ì¸®´Â ÁýÇÕ ¥Ä ÀÇ ¸ðµç ¸ðµ¨ÀÌ ¾î¶² wff ÀÇ ¸ðµ¨ÀÓÀ» ÀÔÁõÇϰíÀÚ ÇÑ´Ù. ÇÏÁö¸¸ ¶§·Î´Â ¥Ä ÀÇ ¸ðµ¨ Áß¿¡¼ ÃÖ¼Ò ÇÑ °³¸¸ ãÀ¸¸é µÇ´Â °æ¿ìµµ ÀÖ´Ù. Áï, ÁýÇÕ ¥Ä ¿¡ ÀÖ´Â wff µéÀÌ ¸ðµÎ °°Àº ÇØ¼®¿¡ ÀÇÇØ ¸¸Á·µÉ ¼ö ÀÖ´Ù´Â °ÍÀ» º¸À̰íÀÚ ÇÏ´Â °ÍÀÌ´Ù. ¹Ù²Ù¾î ¸»Çϸé, ¥Ä ¿¡ ÀÖ´Â ¸ðµç wff ÀÇ ³í¸®°öÀ¸·Î ±¸¼ºµÈ ½ÄÀÇ ¸ðµ¨À» ã°íÀÚ ÇÏ´Â °ÍÀÌ´Ù.
½ÄÀÇ ¸ðµ¨À» ±¸ÇÏ´Â ¹®Á¦¸¦ ¸íÁ¦¸¸Á·¼º (propositional satisfiability, PSAT) ¹®Á¦¶ó°í ÇÑ´Ù. ´ÙÀ½ Àå¿¡¼ ¸ðµç ½ÄÀ» ¸®ÅÍ·²ÀÇ ³í¸®ÇÕ (disjunction) µéÀÇ ³í¸®°ö (conjunction) À¸·Î ³ªÅ¸³¾ ¼ö ÀÖÀ½À» º¸ÀÏ °ÍÀÌ´Ù. ¸®ÅÍ·²ÀÇ ³í¸®ÇÕÀ» Àý (clause) À̶ó°í ºÎ¸£¸ç ÀýÀÇ ³í¸®°öÀ¸·Î Ç¥ÇöµÈ ½ÄÀ» ³í¸®°ö Á¤±ÔÇü (conjunctive normal form, CNF) ¶ó°í ÇÑ´Ù. ±×·¯¹Ç·Î CNF ½Ä¿¡ ´ëÇÏ¿© PSAT ¹®Á¦¸¦ Ç®±â¸¸ ÇÏ¸é µÈ´Ù. Á¦¾àÁ¶°Ç ¸¸Á·, ȸ·Î ÇÕ¼º, ȸ·Î Áø´Ü, °èȹ µîÀÇ Èï¹Ì·Î¿î ¹®Á¦µéÀ» CNF PSAT ¹®Á¦·Î º¯È¯½ÃÄÑ Ç® ¼ö ÀÖ´Ù ([Selman, Kautz, & Cohen 1994]).
CNF PSAT ¹®Á¦¸¦ Ǫ´Â ¼Ò¸ðÀûÀÎ ¹æ¹ýÀº ½ÄÀÇ °¢ ¾ÆÅè¿¡ True ³ª False ¸¦ ÇÒ´çÇÏ´Â ¸ðµç °æ¿ì¸¦ ´Ù ÇØº¸¸é¼ ¸ðµç ÀýÀÌ True °ªÀ» °®´Â °æ¿ì°¡ ÀÖ´ÂÁö È®ÀÎÇÏ´Â °ÍÀÌ´Ù. ½Ä¿¡ n °³ÀÇ ¾ÆÅèÀÌ ÀÖÀ¸¸é ÇÒ´ç ¹æ¹ýÀÌ 2©ú°¡Áö ÀÖÀ¸¹Ç·Î n ÀÌ Ä¿Áö¸é ÀÌ¿Í °°Àº ¼Ò¸ðÀûÀÎ ¹æ¹ýÀ¸·Î´Â °è»êÀÌ ºÒ°¡´ÉÇØÁú ¼ö ÀÖ´Ù.
PSAT ¹®Á¦ÀÇ µÎ °¡Áö Èï¹ÌÀÖ´Â »ç·Ê´Â 2SAT °ú 3SAT ÀÌ´Ù. kSAT ¹®Á¦´Â ÀýÀÌ ÃÖ´ë k ¸®ÅÍ·²À» Æ÷ÇÔÇÏ´Â °æ¿ì¿¡ ÀýÀÇ ³í¸®°öÀÇ ¸ðµ¨À» ±¸ÇÏ´Â ¹®Á¦ÀÌ´Ù. 2SAT ¹®Á¦´Â ´ÙÇ× ½Ã°£ (polynomial) º¹ÀâµµÀÎ ¹Ý¸é, 3SAT ¹®Á¦´Â NP-complete ÀÌ´Ù. ±×·¯¹Ç·Î ÀϹÝÀûÀÎ PSAT ¹®Á¦´Â NP-complete ÀÌ´Ù. ±×·¯³ª ºñ·Ï PSAT °ú °°ÀÌ ¾î¶² ¹®Á¦¿¡ ´ëÇÑ ¸ðµç ¾Ë·ÁÁø ¾Ë°í¸®ÁòµéÀÌ ÃÖ¾ÇÀÇ °æ¿ì Áö¼ö ÇÔ¼öÀûÀÎ ½Ã°£ÀÌ ¼Ò¿äµÈ´Ù°í ÇÏ´õ¶óµµ, ¸¹Àº °æ¿ì¿¡ Æò±Õ ½Ã°£Àº ´ÙÇ× ½Ã°£¸¸ÀÌ °É¸°´Ù. ½ÇÁ¦·Î ¿©·¯ °¡Áö ÀÚ¿¬½º·¯¿î È®·ü ºÐÆ÷¿¡ ´ëÇØ¼ PSAT ¹®Á¦´Â Æò±ÕÀûÀ¸·Î ´ÙÇ× ½Ã°£ÀÌ °É¸°´Ù [Goldberg 1979, Purdom & Brown 1987].
GSAT ´Â ºñ¼Ò¸ðÀûÀ̰í, Ž¿åÀûÀÎ (greedy), ¾ð´ö ¿À¸£±â (hill-climbing) ŸÀÔÀÇ Å½»ö ¹æ¹ýÀÌ´Ù [Selman, Levesque, & Mitchell 1992, Selman & Kautz 1993]. ÀÌ ¹æ¹ýÀº ½ÄÀÇ ¸ðµç ¾ÆÅè¿¡ ´ëÇØ ¹«ÀÛÀ§·Î Á¤ÇÑ °ªÀÇ ÁýÇÕÀ¸·ÎºÎÅÍ ½ÃÀÛÇÑ´Ù. ÀÌ °ªÀÇ ÁýÇÕÀÌ ¹Ù·Î ÇØ¼®ÀÌ´Ù. ÀÌ ÇØ¼® ¾Æ·¡ True °ªÀ» °®´Â ÀýÀÇ ¼ö¸¦ ±â¾ïÇÑ´Ù. ´ÙÀ½Àº °¢ ¾ÆÅèÀ» Â÷·Ê·Î º¸¸é¼ ±× ¾ÆÅèÀÇ °ªÀÌ º¯ÇÏ¸é ¸î °³ÀÇ ÀýÀÌ ´õ True °¡ µÇ´ÂÁö¸¦ °è»êÇÑ´Ù. °¡Àå Áõ°¡ºÐÀÌ Å« ¾ÆÅèÀÇ °ªÀ» º¯°æ½Ã۰í ÀÌ¿Í °°Àº ÀÛ¾÷À» °è¼ÓÇÑ´Ù. ¹°·Ð °¡Àå Å« Áõ°¡ºÐÀÌ 0 À̳ª À½¼ö°¡ µÉ ¼öµµ ÀÖÁö¸¸ GSAT Àº ¾î¶² °æ¿ì¿¡µµ ÇÑ ¾ÆÅèÀÇ °ªÀ» º¯°æÇÑ´Ù. ÀÌ ÀýÂ÷´Â Æò¿ø (plateau) ¿¡¼ ³¡¾øÀÌ Çì¸È ¼öµµ ÀÖÀ¸¹Ç·Î, ÀÏÁ¤ÇÑ ¼ö¸¸ÅÀÇ º¯°æÀ» ÇÏ°í ³ª¸é Á¾·áÇÑ´Ù. ¶ÇÇÑ ÀÌ ÀýÂ÷´Â Áö¿ª ÃÖ´ë°ª (local maximum, ÀϺÎÀÇ Àý¸¸ ¸¸Á·ÇÏ´Â ÇØ¼®) ¿¡¼ Á¾·áµÉ ¼ö ÀÖÀ¸¹Ç·Î, ÀÌ·² ¶§´Â ´õ ³ªÀº ÃÖ´ë°ªÀ» ã±â À§ÇØ ´Ù¸¥ ¹«ÀÛÀ§ ÇØ¼®¿¡¼ ´Ù½Ã ½ÃÀÛÇØ¾ß ÇÒ ¼öµµ ÀÖ´Ù. GSAT ´Â 2000 °³ÀÇ º¯¼ö¸¦ °¡Áø ¹«ÀÛÀ§·Î »ý¼ºµÈ 3SAT ¹®Á¦¿¡ ´ëÇØ ¸ðµ¨À» ãÀ» ¼ö ÀÖ¾úÀ¸¸ç, ¹æ´ëÇÑ N-Äý ¹®Á¦¸¦ ¸íÁ¦·Î º¯È¯ÇÑ ¹®Á¦¸¦ Ǫ´Â µ¥¿¡µµ ÀÌ¿ëµÇ¾ú´Ù. ÀÓÀÇ ÁøÇà ÇüÅ·ΠGSAT ¸¦ ¼öÁ¤ÇÑ WALKSAT °ú °°Àº ¾Ë°í¸®ÁòÀº È¿°ú¸¦ Çâ»ó½ÃŲ´Ù´Â °ÍÀÌ È®ÀεǾú´Ù [Selman, Kautz & Cohen 1994, Selman, Kautz & Cohen 1996].
¸íÁ¦³í¸®´Â Àΰø ¿¡ÀÌÀüÆ®°¡ ÀÚ½ÅÀÇ ¼¼»óÀ» Ç¥ÇöÇϱâ
À§ÇØ »ç¿ëÇÏ´Â °ø½ÄÀûÀÎ ¾ð¾îÀÌ´Ù. Ȥ½Ã ¼öÇаú ÀÚ¿¬¾ð¾î (¸íÁ¦³í¸®¸¦ ¼³¸íÇϱâ À§ÇØ
ÀÌ Ã¥¿¡¼ »ç¿ëÇϰí ÀÖ´Â) ÀÇ ºñ°ø½ÄÀûÀÎ ¾ð¾î¸¦ ¸íÁ¦³í¸® ÀÚüÀÇ °ø½ÄÀûÀÎ ¾ð¾î¿Í
È¥µ¿ÇÒ ¼öµµ ÀÖ´Ù. ¿¹¸¦ µé¾î, {P, P ¡ù Q} ¦§ Q ¶ó°í ¸»ÇÒ ¶§, ¿ì¸®´Â ±âÈ£
¦§ ¸¦ »ç¿ëÇÑ´Ù. ÀÌ ±âÈ£´Â ¸íÁ¦³í¸® ¾ð¾îÀÇ ±âÈ£°¡ ¾Æ´Ï°í ¸íÁ¦³í¸®¸¦ À̾߱âÇϱâ
À§ÇØ »ç¿ëµÇ´Â ¿ì¸® ¾ð¾îÀÇ ±âÈ£ÀÌ´Ù. ¸ÞŸ ¾ð¾î ±âÈ£ ³ª
¸¦ ±âÈ£ ¡ù ¿Í È¥µ¿ÇÏ¸é ¾ÈµÈ´Ù.
¸íÁ¦³í¸®ÀÇ Á¤¸® (Ãß·Ð ±ÔÄ¢¿¡ ÀÇÇØ »ý¼ºµÇ´Â) À̿ܿ¡ ¸íÁ¦³í¸®¿¡ ´ëÇÑ Á¤¸®°¡ Àִµ¥ À̸¦ ¸ÞŸÁ¤¸® (metatheorem) ¶ó°í ºÎ¸¥´Ù. ´ÙÀ½Àº ¸íÁ¦³í¸®¿¡ ´ëÇÑ Áß¿äÇÑ µÎ °¡Áö Á¤¸®ÀÌ´Ù.
2Ç× ¿¬°áÀÚ ¡ü °ú ¡ý ´Â °áÇÕ ¹ýÄ¢ÀÌ ¼º¸³µÈ´Ù. Áï,
±×·¯¹Ç·Î À§ÀÇ wff ¿¡¼ °ýÈ£¸¦ »©°í ´ÙÀ½°ú °°ÀÌ ¾µ ¼ö ÀÖ´Ù.
óÀ½ °ÍÀ» ³í¸®°ö (conjunction), µÎ¹øÂ°¸¦ ³í¸®ÇÕ
(disjunction) À̶ó°í ÇÑ´Ù. óÀ½ wff ¿¡ ÀÖ´Â µéÀ» ³í¸®°ö ÀÎÀÚ (conjunct) ¶ó°í Çϸç, µÎ ¹øÂ° wff ¿¡ ÀÖ´Â °ÍµéÀ» ³í¸®ÇÕ
ÀÎÀÚ (disjunct) ¶ó°í ÇÑ´Ù.