date: 2021-07-08T01:50:32Z pdf:PDFVersion: 1.5 pdf:docinfo:title: A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic xmp:CreatorTool: LaTeX with hyperref access_permission:can_print_degraded: true subject: dc:format: application/pdf; version=1.5 pdf:docinfo:creator_tool: LaTeX with hyperref access_permission:fill_in_form: true pdf:encrypted: false dc:title: A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic modified: 2021-07-08T01:50:32Z cp:subject: pdf:docinfo:subject: pdf:docinfo:creator: Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Kroetzsch, Christoph Weidenbach PTEX.Fullbanner: This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020) kpathsea version 6.3.2 meta:author: Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Kroetzsch, Christoph Weidenbach trapped: False meta:creation-date: 2021-07-08T01:50:32Z created: 2021-07-08T01:50:32Z access_permission:extract_for_accessibility: true Creation-Date: 2021-07-08T01:50:32Z Author: Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Kroetzsch, Christoph Weidenbach producer: pdfTeX-1.40.21 pdf:docinfo:producer: pdfTeX-1.40.21 pdf:unmappedUnicodeCharsPerPage: 0 Keywords: Datalog, arithmetic constraints, Bernays-Schoenfinkel first-order logic, SUPERLOG, SMT access_permission:modify_annotations: true dc:creator: Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Kroetzsch, Christoph Weidenbach dcterms:created: 2021-07-08T01:50:32Z Last-Modified: 2021-07-08T01:50:32Z dcterms:modified: 2021-07-08T01:50:32Z title: A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic Last-Save-Date: 2021-07-08T01:50:32Z pdf:docinfo:keywords: Datalog, arithmetic constraints, Bernays-Schoenfinkel first-order logic, SUPERLOG, SMT pdf:docinfo:modified: 2021-07-08T01:50:32Z meta:save-date: 2021-07-08T01:50:32Z pdf:docinfo:custom:PTEX.Fullbanner: This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020) kpathsea version 6.3.2 Content-Type: application/pdf X-Parsed-By: org.apache.tika.parser.DefaultParser creator: Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Kroetzsch, Christoph Weidenbach dc:subject: Datalog, arithmetic constraints, Bernays-Schoenfinkel first-order logic, SUPERLOG, SMT access_permission:assemble_document: true xmpTPg:NPages: 26 pdf:charsPerPage: 1113 access_permission:extract_content: true access_permission:can_print: true pdf:docinfo:trapped: False meta:keyword: Datalog, arithmetic constraints, Bernays-Schoenfinkel first-order logic, SUPERLOG, SMT access_permission:can_modify: true pdf:docinfo:created: 2021-07-08T01:50:32Z