Knowledge (XXG)

CADE ATP System Competition

Source πŸ“

307: 47: 394:
Moser, Max; Ibens, Ortrun; Letz, Reinhold; Steinbach, Joachim; Goller, Christoph; Schumann, Johann; Mayr, Klaus (1997). "Otter-the CADE-13 competition incarnations".
452: 457: 338: 252: 51: 43: 90: 359: 55: 231: 197: 432: 145: 28: 54:. It has inspired similar competition in related fields, in particular the successful SMT-COMP competition for 316: 269: 74: 321: 59: 411: 376: 174: 111: 70: 223: 334: 248: 403: 368: 326: 281: 240: 123: 78: 69:
The first CASC, CASC-13, was held as part of the 13th Conference on Automated Deduction at
308:
International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
141: 32: 354: 446: 302: 380: 415: 63: 407: 372: 286: 268:
Matti, JΓ€rvisalo; Le Berre, Daniel; Roussel, Olivier; Simon, Laurent (2012).
303:"Design and results of TANCS-2000 non-classical (modal) systems comparison" 127: 330: 244: 149: 112:"The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5" 357:; Wos, Larry (1997). "Otter-the CADE-13 competition incarnations". 73:, New Brunswick, NJ, in 1996. Among the systems competing were 196:
Jeff Pelletier, Geoff Sutcliffe and Christian Suttner (2002).
222:
Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005).
437: 224:"SMT-COMP: Satisfiability Modulo Theories Competition" 48:
International Joint Conference on Automated Reasoning
301:Massacci, Fabio; Donini, Francesco M. (2000). 173:Geoff Sutcliffe and Christian Suttner (2006). 168: 166: 8: 16:Annual automated theorem proving competition 270:"The international SAT solver competitions" 320: 285: 102: 311:. Lecture Notes in Computer Science. 235:. Lecture Notes in Computer Science. 7: 453:Artificial intelligence competitions 27:) is an annual competition of fully 52:Association for Automated Reasoning 14: 146:"The CADE ATP System Competition" 44:Conference on Automated Deduction 433:Archive of original CASC website 91:List of computer science awards 396:Journal of Automated Reasoning 360:Journal of Automated Reasoning 56:satisfiability modulo theories 1: 458:Computer science competitions 42:CASC is associated with the 232:Computer Aided Verification 21:CADE ATP System Competition 474: 58:, the SAT Competition for 198:"The Development of CASC" 110:Sutcliffe, Geoff (2011). 29:automated theorem provers 287:10.1609/aimag.v33i1.2395 408:10.1023/A:1005808119103 373:10.1023/A:1005843632307 66:reasoning competition. 128:10.3233/AIC-2010-0483 315:. Springer: 52–56. 239:. Springer: 20–23. 175:"The State of CASC" 62:reasoners, and the 331:10.1007/10722086_4 245:10.1007/11513988_4 71:Rutgers University 340:978-3-540-67697-3 254:978-3-540-27231-1 205:AI Communications 179:AI Communications 116:AI Communications 50:organized by the 465: 420: 419: 391: 385: 384: 351: 345: 344: 324: 298: 292: 291: 289: 265: 259: 258: 228: 219: 213: 212: 202: 193: 187: 186: 170: 161: 160: 158: 157: 148:. Archived from 138: 132: 131: 107: 473: 472: 468: 467: 466: 464: 463: 462: 443: 442: 429: 424: 423: 393: 392: 388: 355:McCune, William 353: 352: 348: 341: 322:10.1.1.385.6267 300: 299: 295: 267: 266: 262: 255: 226: 221: 220: 216: 200: 195: 194: 190: 172: 171: 164: 155: 153: 142:Geoff Sutcliffe 140: 139: 135: 109: 108: 104: 99: 87: 40: 33:classical logic 17: 12: 11: 5: 471: 469: 461: 460: 455: 445: 444: 441: 440: 435: 428: 427:External links 425: 422: 421: 402:(2): 237–246. 386: 367:(2): 211–220. 346: 339: 293: 260: 253: 214: 188: 162: 133: 101: 100: 98: 95: 94: 93: 86: 83: 39: 36: 15: 13: 10: 9: 6: 4: 3: 2: 470: 459: 456: 454: 451: 450: 448: 439: 436: 434: 431: 430: 426: 417: 413: 409: 405: 401: 397: 390: 387: 382: 378: 374: 370: 366: 362: 361: 356: 350: 347: 342: 336: 332: 328: 323: 318: 314: 310: 309: 304: 297: 294: 288: 283: 279: 275: 271: 264: 261: 256: 250: 246: 242: 238: 234: 233: 225: 218: 215: 211:(2–3): 79–90. 210: 206: 199: 192: 189: 184: 180: 176: 169: 167: 163: 152:on 2009-03-02 151: 147: 143: 137: 134: 129: 125: 121: 117: 113: 106: 103: 96: 92: 89: 88: 84: 82: 80: 76: 72: 67: 65: 61: 60:propositional 57: 53: 49: 45: 37: 35: 34: 30: 26: 22: 438:CASC Website 399: 395: 389: 364: 358: 349: 312: 306: 296: 280:(1): 89–92. 277: 273: 263: 236: 230: 217: 208: 204: 191: 182: 178: 154:. Retrieved 150:the original 136: 122:(1): 75–89. 119: 115: 105: 68: 41: 24: 20: 18: 274:AI Magazine 185:(1): 35–48. 64:modal logic 38:Competition 447:Categories 156:2008-10-23 97:References 317:CiteSeerX 85:See also 46:and the 381:2481653 416:821198 414:  379:  337:  319:  251:  79:SETHEO 412:S2CID 377:S2CID 227:(PDF) 201:(PDF) 75:Otter 335:ISBN 313:1847 249:ISBN 237:3576 77:and 31:for 25:CASC 19:The 404:doi 369:doi 327:doi 282:doi 241:doi 124:doi 449:: 410:. 400:18 398:. 375:. 365:18 363:. 333:. 325:. 305:. 278:33 276:. 272:. 247:. 229:. 209:15 207:. 203:. 183:19 181:. 177:. 165:^ 144:. 120:24 118:. 114:. 81:. 418:. 406:: 383:. 371:: 343:. 329:: 290:. 284:: 257:. 243:: 159:. 130:. 126:: 23:(

Index

automated theorem provers
classical logic
Conference on Automated Deduction
International Joint Conference on Automated Reasoning
Association for Automated Reasoning
satisfiability modulo theories
propositional
modal logic
Rutgers University
Otter
SETHEO
List of computer science awards
"The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5"
doi
10.3233/AIC-2010-0483
Geoff Sutcliffe
"The CADE ATP System Competition"
the original


"The State of CASC"
"The Development of CASC"
"SMT-COMP: Satisfiability Modulo Theories Competition"
Computer Aided Verification
doi
10.1007/11513988_4
ISBN
978-3-540-27231-1
"The international SAT solver competitions"
doi

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

↑