Knowledge

Yale shooting problem

Source đź“ť

25: 1766:
was to include a new condition of occlusion, which formalizes the “permission to change” for a fluent. The effect of an action that might change a fluent is therefore that the fluent has the new value, and that the occlusion is made (temporarily) true. What is minimized is not the set of changes, but
853:
An early solution to the frame problem was based on minimizing the changes. In other words, the scenario is formalized by the formulae above (that specify only the effects of actions) and by the assumption that the changes in the fluents over time are as minimal as possible. The rationale is that the
706:
is consistent with all these formulae, although there is no reason to believe that Fred dies before the gun has been shot. The problem is that the formulae above only include the effects of actions, but do not specify that all fluents not changed by the actions remain the same. In other words, a
153:
is formalized in logic by minimizing the changes in this situation, then it cannot be uniquely proved that Fred is dead after loading, waiting, and shooting. In one solution, Fred indeed dies; in another (also logically correct) solution, the gun becomes mysteriously unloaded and Fred survives.
1793:. In spite of being a solved problem, that example is still sometimes mentioned in recent research papers, where it is used as an illustrative example (e.g., for explaining the syntax of a new logic for reasoning about actions), rather than being presented as a problem. 1730:
While the Yale shooting problem has been considered a severe obstacle to the use of logic for formalizing dynamical scenarios, solutions to it have been known since the late 1980s. One solution involves the use of
232:. Initially, the first condition is true and the second is false. Then, the gun is loaded, some time passes, and the gun is fired. Such problems can be formalized in logic by considering four time points 610: 535: 1692:
becomes true at time 1 and false at time 2. As a result, this evaluation is considered a valid description of the evolution of the state, although there is no valid reason to explain
773: 655:. This is a simplified formalization in which action names are neglected and the effects of actions are directly specified for the time points in which the actions are executed. See 1650: 1602: 1509: 1080: 475: 1030: 704: 1862:
R. Reiter (1991). The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. In Vladimir Lifschitz, editor,
1554: 1215: 1170: 1125: 1459: 1417: 1375: 1333: 985: 943: 901: 427: 383: 1725: 1690: 1255: 812: 230: 149:) is initially alive and a gun is initially unloaded. Loading the gun, waiting for a moment, and then shooting the gun at Fred is expected to kill Fred. However, if 1287: 844: 342: 195: 653: 633: 310: 290: 270: 250: 1759:
statement, the effects of shooting are correctly formalized. (Predicate completion is more complicated when there is more than one implication involved.)
1727:
being false at time 2. The fact that minimization of changes leads to wrong solution is the motivation for the introduction of the Yale shooting problem.
846:. The necessity of a large number of formulae stating the obvious fact that conditions do not change unless an action changes them is known as the 854:
formulae above enforce all effect of actions to take place, while minimization should restrict the changes to exactly those due to the actions.
42: 1767:
the set of occlusions being true. Another constraint specifying that no fluent changes unless occlusion is true completes this solution.
662:
The formulae above, while being direct formalizations of the known facts, do not suffice to correctly characterize the domain. Indeed,
1849: 1891: 1842: 108: 89: 61: 1735:
in the specification of actions: in this solution, the fact that shooting causes Fred to die is formalized by the preconditions:
158: 857:
In the Yale shooting scenario, one possible evaluation of the fluents in which the changes are minimized is the following one.
68: 46: 1833: 541: 615:
The first two formulae represent the initial state. The third formula formalizes the effect of loading the gun at time
385:
depending on time. A direct formalization of the statement of the Yale shooting problem in logic is the following one:
75: 1896: 1783: 1886: 57: 481: 1790: 710: 1802: 35: 1732: 1608: 1560: 1467: 1038: 433: 1859:
T. Mitchell and H. Levesque (2006). The 2005 AAAI Classic Paper awards. "AI Magazine", 26(4):98–99.
991: 665: 82: 1828: 1812: 1775: 656: 134: 1864:
Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy
1515: 1176: 1131: 1086: 1423: 1381: 1339: 1297: 949: 907: 865: 391: 347: 1789:
In 2005, the 1985 paper in which the Yale shooting scenario was first described received the
1695: 1660: 1225: 782: 200: 1260: 817: 315: 168: 1824: 1779: 142: 1763: 638: 618: 295: 275: 255: 235: 138: 1880: 1807: 1289:
becomes false at time 3. The following evaluation also satisfies all formulae above.
847: 146: 130: 162: 133:
fail. The name of this problem comes from a scenario proposed by its inventors,
24: 1852:(1986). Applications of circumscription to formalizing common-sense knowledge. 1840:
S. Hanks and D. McDermott (1987). Nonmonotonic logic and temporal projection.
1771: 775:
must be added to formalize the implicit assumption that loading the gun
635:. The fourth formula formalizes the effect of shooting at Fred at time 150: 145:
when they proposed it. In this scenario, Fred (later identified as a
126: 1770:
The Yale shooting scenario is also correctly formalized by the
1222:
This is the expected solution. It contains two fluent changes:
18: 1831:(1993). Representing action and change by logic programs. 1657:
In this evaluation, there are still two changes only:
1755:
becoming false). By turning this implication into an
1698: 1663: 1611: 1563: 1518: 1470: 1426: 1384: 1342: 1300: 1263: 1228: 1179: 1134: 1089: 1041: 994: 952: 910: 868: 820: 785: 713: 668: 641: 621: 544: 484: 436: 394: 350: 318: 298: 278: 258: 238: 203: 171: 49:. Unsourced material may be challenged and removed. 1719: 1684: 1644: 1596: 1548: 1503: 1453: 1411: 1369: 1327: 1281: 1249: 1209: 1164: 1119: 1074: 1024: 979: 937: 895: 838: 806: 767: 698: 647: 627: 605:{\displaystyle loaded(2)\rightarrow \neg alive(3)} 604: 529: 469: 421: 377: 336: 304: 284: 264: 244: 224: 189: 125:is a conundrum or scenario in formal situational 157:Technically, this scenario is described by two 8: 1866:, pages 359–380. Academic Press, New York. 1697: 1662: 1610: 1562: 1517: 1469: 1425: 1383: 1341: 1299: 1262: 1227: 1178: 1133: 1088: 1040: 993: 951: 909: 867: 819: 784: 712: 667: 640: 620: 543: 530:{\displaystyle true\rightarrow loaded(1)} 483: 435: 393: 349: 317: 297: 277: 257: 237: 202: 170: 161:(a fluent is a condition that can change 109:Learn how and when to remove this message 129:on which early logical solutions to the 768:{\displaystyle alive(0)\equiv alive(1)} 1751:was true before, this corresponds to 7: 47:adding citations to reliable sources 312:, and turning every fluent such as 1612: 1564: 1471: 1042: 995: 669: 575: 437: 14: 1291: 859: 23: 34:needs additional citations for 1645:{\displaystyle \neg loaded(3)} 1639: 1633: 1597:{\displaystyle \neg loaded(2)} 1591: 1585: 1543: 1537: 1504:{\displaystyle \neg loaded(0)} 1498: 1492: 1448: 1442: 1406: 1400: 1364: 1358: 1322: 1316: 1204: 1198: 1159: 1153: 1114: 1108: 1075:{\displaystyle \neg loaded(0)} 1069: 1063: 1019: 1013: 974: 968: 932: 926: 890: 884: 762: 756: 735: 729: 693: 687: 599: 593: 572: 569: 563: 524: 518: 497: 470:{\displaystyle \neg loaded(0)} 464: 458: 416: 410: 372: 366: 1: 1025:{\displaystyle \neg alive(3)} 699:{\displaystyle \neg alive(1)} 1834:Journal of Logic Programming 1784:action description languages 1257:becomes true at time 1 and 1913: 1873:. Oxford University Press. 1743:, and the effect is that 1549:{\displaystyle loaded(1)} 1210:{\displaystyle loaded(3)} 1165:{\displaystyle loaded(2)} 1120:{\displaystyle loaded(1)} 1892:Knowledge representation 1791:AAAI Classic Paper award 1454:{\displaystyle alive(3)} 1412:{\displaystyle alive(2)} 1370:{\displaystyle alive(1)} 1328:{\displaystyle alive(0)} 980:{\displaystyle alive(2)} 938:{\displaystyle alive(1)} 896:{\displaystyle alive(0)} 422:{\displaystyle alive(0)} 378:{\displaystyle alive(t)} 1854:Artificial Intelligence 1843:Artificial Intelligence 1803:Circumscription (logic) 1762:A solution proposed by 58:"Yale shooting problem" 16:Problem in formal logic 1721: 1720:{\displaystyle loaded} 1686: 1685:{\displaystyle loaded} 1646: 1598: 1550: 1505: 1455: 1413: 1371: 1329: 1283: 1251: 1250:{\displaystyle loaded} 1211: 1166: 1121: 1076: 1026: 981: 939: 897: 840: 808: 807:{\displaystyle loaded} 769: 700: 649: 629: 606: 531: 471: 423: 379: 338: 306: 286: 266: 246: 226: 225:{\displaystyle loaded} 191: 1869:E. Sandewall (1994). 1747:changes value (since 1722: 1687: 1647: 1599: 1551: 1506: 1456: 1414: 1372: 1330: 1284: 1282:{\displaystyle alive} 1252: 1212: 1167: 1122: 1077: 1027: 982: 940: 898: 841: 839:{\displaystyle alive} 814:and not the value of 809: 779:changes the value of 770: 701: 650: 630: 607: 532: 472: 424: 380: 339: 337:{\displaystyle alive} 307: 287: 267: 247: 227: 192: 190:{\displaystyle alive} 123:Yale shooting problem 1871:Features and Fluents 1733:predicate completion 1696: 1661: 1609: 1561: 1516: 1468: 1424: 1382: 1340: 1298: 1261: 1226: 1177: 1132: 1087: 1039: 992: 950: 908: 866: 818: 783: 711: 666: 639: 619: 542: 482: 434: 392: 348: 316: 296: 276: 256: 236: 201: 169: 43:improve this article 1897:1987 introductions 1813:Situation calculus 1776:situation calculus 1717: 1682: 1642: 1594: 1546: 1501: 1451: 1409: 1367: 1325: 1279: 1247: 1207: 1162: 1117: 1072: 1022: 977: 935: 893: 836: 804: 765: 696: 657:situation calculus 645: 625: 602: 527: 467: 419: 375: 334: 302: 282: 262: 242: 222: 187: 1887:Logic programming 1655: 1654: 1220: 1219: 648:{\displaystyle 2} 628:{\displaystyle 0} 344:into a predicate 305:{\displaystyle 3} 285:{\displaystyle 2} 265:{\displaystyle 1} 245:{\displaystyle 0} 119: 118: 111: 93: 1904: 1846:, 33(3):379–412. 1726: 1724: 1723: 1718: 1691: 1689: 1688: 1683: 1651: 1649: 1648: 1643: 1603: 1601: 1600: 1595: 1555: 1553: 1552: 1547: 1510: 1508: 1507: 1502: 1460: 1458: 1457: 1452: 1418: 1416: 1415: 1410: 1376: 1374: 1373: 1368: 1334: 1332: 1331: 1326: 1292: 1288: 1286: 1285: 1280: 1256: 1254: 1253: 1248: 1216: 1214: 1213: 1208: 1171: 1169: 1168: 1163: 1126: 1124: 1123: 1118: 1081: 1079: 1078: 1073: 1031: 1029: 1028: 1023: 986: 984: 983: 978: 944: 942: 941: 936: 902: 900: 899: 894: 860: 845: 843: 842: 837: 813: 811: 810: 805: 774: 772: 771: 766: 705: 703: 702: 697: 654: 652: 651: 646: 634: 632: 631: 626: 611: 609: 608: 603: 536: 534: 533: 528: 476: 474: 473: 468: 428: 426: 425: 420: 384: 382: 381: 376: 343: 341: 340: 335: 311: 309: 308: 303: 291: 289: 288: 283: 271: 269: 268: 263: 251: 249: 248: 243: 231: 229: 228: 223: 196: 194: 193: 188: 114: 107: 103: 100: 94: 92: 51: 27: 19: 1912: 1911: 1907: 1906: 1905: 1903: 1902: 1901: 1877: 1876: 1821: 1799: 1780:fluent calculus 1774:version of the 1694: 1693: 1659: 1658: 1607: 1606: 1559: 1558: 1514: 1513: 1466: 1465: 1422: 1421: 1380: 1379: 1338: 1337: 1296: 1295: 1259: 1258: 1224: 1223: 1175: 1174: 1130: 1129: 1085: 1084: 1037: 1036: 990: 989: 948: 947: 906: 905: 864: 863: 816: 815: 781: 780: 709: 708: 664: 663: 637: 636: 617: 616: 540: 539: 480: 479: 432: 431: 390: 389: 346: 345: 314: 313: 294: 293: 274: 273: 254: 253: 234: 233: 199: 198: 167: 166: 143:Yale University 115: 104: 98: 95: 52: 50: 40: 28: 17: 12: 11: 5: 1910: 1908: 1900: 1899: 1894: 1889: 1879: 1878: 1875: 1874: 1867: 1860: 1857: 1847: 1838: 1820: 1817: 1816: 1815: 1810: 1805: 1798: 1795: 1764:Erik Sandewall 1757:if and only if 1716: 1713: 1710: 1707: 1704: 1701: 1681: 1678: 1675: 1672: 1669: 1666: 1653: 1652: 1641: 1638: 1635: 1632: 1629: 1626: 1623: 1620: 1617: 1614: 1604: 1593: 1590: 1587: 1584: 1581: 1578: 1575: 1572: 1569: 1566: 1556: 1545: 1542: 1539: 1536: 1533: 1530: 1527: 1524: 1521: 1511: 1500: 1497: 1494: 1491: 1488: 1485: 1482: 1479: 1476: 1473: 1462: 1461: 1450: 1447: 1444: 1441: 1438: 1435: 1432: 1429: 1419: 1408: 1405: 1402: 1399: 1396: 1393: 1390: 1387: 1377: 1366: 1363: 1360: 1357: 1354: 1351: 1348: 1345: 1335: 1324: 1321: 1318: 1315: 1312: 1309: 1306: 1303: 1278: 1275: 1272: 1269: 1266: 1246: 1243: 1240: 1237: 1234: 1231: 1218: 1217: 1206: 1203: 1200: 1197: 1194: 1191: 1188: 1185: 1182: 1172: 1161: 1158: 1155: 1152: 1149: 1146: 1143: 1140: 1137: 1127: 1116: 1113: 1110: 1107: 1104: 1101: 1098: 1095: 1092: 1082: 1071: 1068: 1065: 1062: 1059: 1056: 1053: 1050: 1047: 1044: 1033: 1032: 1021: 1018: 1015: 1012: 1009: 1006: 1003: 1000: 997: 987: 976: 973: 970: 967: 964: 961: 958: 955: 945: 934: 931: 928: 925: 922: 919: 916: 913: 903: 892: 889: 886: 883: 880: 877: 874: 871: 835: 832: 829: 826: 823: 803: 800: 797: 794: 791: 788: 764: 761: 758: 755: 752: 749: 746: 743: 740: 737: 734: 731: 728: 725: 722: 719: 716: 695: 692: 689: 686: 683: 680: 677: 674: 671: 644: 624: 613: 612: 601: 598: 595: 592: 589: 586: 583: 580: 577: 574: 571: 568: 565: 562: 559: 556: 553: 550: 547: 537: 526: 523: 520: 517: 514: 511: 508: 505: 502: 499: 496: 493: 490: 487: 477: 466: 463: 460: 457: 454: 451: 448: 445: 442: 439: 429: 418: 415: 412: 409: 406: 403: 400: 397: 374: 371: 368: 365: 362: 359: 356: 353: 333: 330: 327: 324: 321: 301: 281: 261: 241: 221: 218: 215: 212: 209: 206: 186: 183: 180: 177: 174: 139:Drew McDermott 117: 116: 31: 29: 22: 15: 13: 10: 9: 6: 4: 3: 2: 1909: 1898: 1895: 1893: 1890: 1888: 1885: 1884: 1882: 1872: 1868: 1865: 1861: 1858: 1855: 1851: 1848: 1845: 1844: 1839: 1837:, 17:301–322. 1836: 1835: 1830: 1826: 1823: 1822: 1818: 1814: 1811: 1809: 1808:Frame problem 1806: 1804: 1801: 1800: 1796: 1794: 1792: 1787: 1785: 1781: 1777: 1773: 1768: 1765: 1760: 1758: 1754: 1750: 1746: 1742: 1738: 1734: 1728: 1714: 1711: 1708: 1705: 1702: 1699: 1679: 1676: 1673: 1670: 1667: 1664: 1636: 1630: 1627: 1624: 1621: 1618: 1615: 1605: 1588: 1582: 1579: 1576: 1573: 1570: 1567: 1557: 1540: 1534: 1531: 1528: 1525: 1522: 1519: 1512: 1495: 1489: 1486: 1483: 1480: 1477: 1474: 1464: 1463: 1445: 1439: 1436: 1433: 1430: 1427: 1420: 1403: 1397: 1394: 1391: 1388: 1385: 1378: 1361: 1355: 1352: 1349: 1346: 1343: 1336: 1319: 1313: 1310: 1307: 1304: 1301: 1294: 1293: 1290: 1276: 1273: 1270: 1267: 1264: 1244: 1241: 1238: 1235: 1232: 1229: 1201: 1195: 1192: 1189: 1186: 1183: 1180: 1173: 1156: 1150: 1147: 1144: 1141: 1138: 1135: 1128: 1111: 1105: 1102: 1099: 1096: 1093: 1090: 1083: 1066: 1060: 1057: 1054: 1051: 1048: 1045: 1035: 1034: 1016: 1010: 1007: 1004: 1001: 998: 988: 971: 965: 962: 959: 956: 953: 946: 929: 923: 920: 917: 914: 911: 904: 887: 881: 878: 875: 872: 869: 862: 861: 858: 855: 851: 849: 848:frame problem 833: 830: 827: 824: 821: 801: 798: 795: 792: 789: 786: 778: 759: 753: 750: 747: 744: 741: 738: 732: 726: 723: 720: 717: 714: 690: 684: 681: 678: 675: 672: 660: 659:for details. 658: 642: 622: 596: 590: 587: 584: 581: 578: 566: 560: 557: 554: 551: 548: 545: 538: 521: 515: 512: 509: 506: 503: 500: 494: 491: 488: 485: 478: 461: 455: 452: 449: 446: 443: 440: 430: 413: 407: 404: 401: 398: 395: 388: 387: 386: 369: 363: 360: 357: 354: 351: 331: 328: 325: 322: 319: 299: 279: 259: 239: 219: 216: 213: 210: 207: 204: 184: 181: 178: 175: 172: 164: 160: 155: 152: 148: 144: 141:, working at 140: 136: 132: 131:frame problem 128: 124: 113: 110: 102: 91: 88: 84: 81: 77: 74: 70: 67: 63: 60: â€“  59: 55: 54:Find sources: 48: 44: 38: 37: 32:This article 30: 26: 21: 20: 1870: 1863: 1856:, 28:89–116. 1853: 1841: 1832: 1829:V. Lifschitz 1788: 1769: 1761: 1756: 1752: 1748: 1744: 1740: 1736: 1729: 1656: 1221: 856: 852: 776: 661: 614: 165:over time): 156: 122: 120: 105: 96: 86: 79: 72: 65: 53: 41:Please help 36:verification 33: 1850:J. McCarthy 163:truth value 135:Steve Hanks 1881:Categories 1825:M. Gelfond 1819:References 1782:, and the 69:newspapers 1613:¬ 1565:¬ 1472:¬ 1043:¬ 996:¬ 739:≡ 670:¬ 576:¬ 573:→ 498:→ 438:¬ 99:July 2020 1797:See also 707:formula 159:fluents 151:inertia 83:scholar 1778:, the 1772:Reiter 1741:loaded 292:, and 147:turkey 85:  78:  71:  64:  56:  1753:alive 1749:alive 1745:alive 1737:alive 127:logic 90:JSTOR 76:books 1827:and 1739:and 777:only 197:and 137:and 121:The 62:news 45:by 1883:: 1786:. 850:. 272:, 252:, 1715:d 1712:e 1709:d 1706:a 1703:o 1700:l 1680:d 1677:e 1674:d 1671:a 1668:o 1665:l 1640:) 1637:3 1634:( 1631:d 1628:e 1625:d 1622:a 1619:o 1616:l 1592:) 1589:2 1586:( 1583:d 1580:e 1577:d 1574:a 1571:o 1568:l 1544:) 1541:1 1538:( 1535:d 1532:e 1529:d 1526:a 1523:o 1520:l 1499:) 1496:0 1493:( 1490:d 1487:e 1484:d 1481:a 1478:o 1475:l 1449:) 1446:3 1443:( 1440:e 1437:v 1434:i 1431:l 1428:a 1407:) 1404:2 1401:( 1398:e 1395:v 1392:i 1389:l 1386:a 1365:) 1362:1 1359:( 1356:e 1353:v 1350:i 1347:l 1344:a 1323:) 1320:0 1317:( 1314:e 1311:v 1308:i 1305:l 1302:a 1277:e 1274:v 1271:i 1268:l 1265:a 1245:d 1242:e 1239:d 1236:a 1233:o 1230:l 1205:) 1202:3 1199:( 1196:d 1193:e 1190:d 1187:a 1184:o 1181:l 1160:) 1157:2 1154:( 1151:d 1148:e 1145:d 1142:a 1139:o 1136:l 1115:) 1112:1 1109:( 1106:d 1103:e 1100:d 1097:a 1094:o 1091:l 1070:) 1067:0 1064:( 1061:d 1058:e 1055:d 1052:a 1049:o 1046:l 1020:) 1017:3 1014:( 1011:e 1008:v 1005:i 1002:l 999:a 975:) 972:2 969:( 966:e 963:v 960:i 957:l 954:a 933:) 930:1 927:( 924:e 921:v 918:i 915:l 912:a 891:) 888:0 885:( 882:e 879:v 876:i 873:l 870:a 834:e 831:v 828:i 825:l 822:a 802:d 799:e 796:d 793:a 790:o 787:l 763:) 760:1 757:( 754:e 751:v 748:i 745:l 742:a 736:) 733:0 730:( 727:e 724:v 721:i 718:l 715:a 694:) 691:1 688:( 685:e 682:v 679:i 676:l 673:a 643:2 623:0 600:) 597:3 594:( 591:e 588:v 585:i 582:l 579:a 570:) 567:2 564:( 561:d 558:e 555:d 552:a 549:o 546:l 525:) 522:1 519:( 516:d 513:e 510:d 507:a 504:o 501:l 495:e 492:u 489:r 486:t 465:) 462:0 459:( 456:d 453:e 450:d 447:a 444:o 441:l 417:) 414:0 411:( 408:e 405:v 402:i 399:l 396:a 373:) 370:t 367:( 364:e 361:v 358:i 355:l 352:a 332:e 329:v 326:i 323:l 320:a 300:3 280:2 260:1 240:0 220:d 217:e 214:d 211:a 208:o 205:l 185:e 182:v 179:i 176:l 173:a 112:) 106:( 101:) 97:( 87:· 80:· 73:· 66:· 39:.

Index


verification
improve this article
adding citations to reliable sources
"Yale shooting problem"
news
newspapers
books
scholar
JSTOR
Learn how and when to remove this message
logic
frame problem
Steve Hanks
Drew McDermott
Yale University
turkey
inertia
fluents
truth value
situation calculus
frame problem
predicate completion
Erik Sandewall
Reiter
situation calculus
fluent calculus
action description languages
AAAI Classic Paper award
Circumscription (logic)

Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.

↑