{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T06:21:25Z","timestamp":1775283685437,"version":"3.50.1"},"reference-count":0,"publisher":"IOS Press","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"abstract":"<jats:p>Applications in artificial intelligence, formal verification, and other areas have greatly benefited from the recent advances in SAT. It is often the case, however, that applications in these fields require determining the satisfiability of formulas in more expressive logics such as first-order logic. Also, these applications typically require not general first-order satisfiability, but rather satisfiability with respect to some background theory, which fixes the interpretations of certain predicate and function symbols.<\/jats:p>","DOI":"10.3233\/978-1-58603-929-5-825","type":"book-chapter","created":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T06:58:24Z","timestamp":1740380304000},"source":"Crossref","is-referenced-by-count":34,"title":["Satisfiability Modulo Theories"],"prefix":"10.3233","author":[{"family":"Barrett Clark","sequence":"additional","affiliation":[]},{"family":"Sebastiani Roberto","sequence":"additional","affiliation":[]},{"family":"Seshia Sanjit A.","sequence":"additional","affiliation":[]},{"family":"Tinelli Cesare","sequence":"additional","affiliation":[]}],"member":"7437","container-title":["Frontiers in Artificial Intelligence and Applications","Handbook of Satisfiability"],"original-title":[],"deposited":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T07:15:44Z","timestamp":1740381344000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospressISSNISBN&issn=0922-6389&volume=185&spage=825"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/978-1-58603-929-5-825","relation":{"is-cited-by":[{"id-type":"doi","id":"10.4204\/EPTCS.257.6","asserted-by":"object"},{"id-type":"doi","id":"10.1007\/JHEP02(2019)058","asserted-by":"object"},{"id-type":"doi","id":"10.4204\/EPTCS.234.6","asserted-by":"object"},{"id-type":"doi","id":"10.1007\/978-3-030-88494-9_11","asserted-by":"object"},{"id-type":"doi","id":"10.1007\/978-3-030-57628-8_10","asserted-by":"object"},{"id-type":"doi","id":"10.4204\/EPTCS.256.14","asserted-by":"object"},{"id-type":"doi","id":"10.4204\/EPTCS.267.2","asserted-by":"object"},{"id-type":"doi","id":"10.1007\/978-3-030-02508-3_15","asserted-by":"object"},{"id-type":"doi","id":"10.1007\/978-3-030-30923-7_10","asserted-by":"object"},{"id-type":"doi","id":"10.1145\/3377930.3389807","asserted-by":"object"},{"id-type":"doi","id":"10.4204\/EPTCS.345.15","asserted-by":"object"},{"id-type":"doi","id":"10.1007\/978-3-030-95312-6_11","asserted-by":"object"},{"id-type":"doi","id":"10.1007\/978-3-319-99725-4_4","asserted-by":"object"},{"id-type":"doi","id":"10.4204\/EPTCS.325.25","asserted-by":"object"},{"id-type":"doi","id":"10.4204\/EPTCS.297.7","asserted-by":"object"},{"id-type":"doi","id":"10.1007\/s10817-020-09571-y","asserted-by":"object"},{"id-type":"doi","id":"10.4204\/EPTCS.250.2","asserted-by":"object"}]},"ISSN":["0922-6389"],"issn-type":[{"value":"0922-6389","type":"print"}],"subject":[],"published":{"date-parts":[[2009]]}}}