@prefix dcat: <http://www.w3.org/ns/dcat#> .
@prefix dct: <http://purl.org/dc/terms/> .
@prefix foaf: <http://xmlns.com/foaf/0.1/> .
@prefix vcard: <http://www.w3.org/2006/vcard/ns#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .

<https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-hal-00703207v1> a dcat:Dataset ;
    dct:description """
              SMT solvers can decide the satisfiability of ground formulas modulo a combination of built-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures. In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate on two examples, how such proofs can be achieved in our formalism.
            """ ;
    dct:identifier "Report N°: RR-7986" ;
    dct:issued "2026-05-16T09:45:44.101971"^^xsd:dateTime ;
    dct:language "en" ;
    dct:modified "2026-05-16T09:45:44.101976"^^xsd:dateTime ;
    dct:publisher <https://rec.harvest-normandie.data4citizen.com/organization/cce9db95-46d9-4dc2-84b6-764215d0a002> ;
    dct:title "Reasoning with Triggers" ;
    dcat:contactPoint [ a vcard:Organization ;
            vcard:fn "CCSD" ] ;
    dcat:distribution <https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-hal-00703207v1/resource/379cc2ce-87c2-4aea-91ba-7794122be9f4> ;
    dcat:keyword "infoeu-reposemanticsreport",
        "infoinfo-clcomputer-science-cscomputation-and-language-cscl",
        "quantifiers",
        "reports",
        "smt-solvers",
        "theories",
        "triggers" ;
    dcat:landingPage <https://inria.hal.science/hal-00703207> .

<https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-hal-00703207v1/resource/379cc2ce-87c2-4aea-91ba-7794122be9f4> a dcat:Distribution ;
    dct:format "HTML" ;
    dct:issued "2026-05-16T09:45:44.117637"^^xsd:dateTime ;
    dct:modified "2026-05-16T09:45:44.082633"^^xsd:dateTime ;
    dct:title "Reasoning with Triggers" ;
    dcat:accessURL <https://inria.hal.science/hal-00703207> .

<https://rec.harvest-normandie.data4citizen.com/organization/cce9db95-46d9-4dc2-84b6-764215d0a002> a foaf:Agent ;
    foaf:name "test_moissonnage_selune" .

<https://inria.hal.science/hal-00703207> a foaf:Document .