@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-00779199v4> a dcat:Dataset ;
    dct:description """
              In this paper, we introduce two focussed sequent calculi, LKp(T) and LK+(T), that are based on Miller-Liang's LKF system for polarised classical logic. The novelty is that those sequent calculi integrate the possibility to call a decision procedure for some background theory T, and the possibility to polarise literals "on the fly" during proof-search. These features are used in our other works to simulate the DPLL(T) procedure as proof-search in the extension of LKp(T) with a cut-rule. In this report we therefore prove cut-elimination in LKp(T). Contrary to what happens in the empty theory, the polarity of literals affects the provability of formulae in presence of a theory T. On the other hand, changing the polarities of connectives does not change the provability of formulae, only the shape of proofs. In order to prove this, we introduce a second sequent calculus, LK+(T) that extends LKp(T) with a relaxed focussing discipline, but we then show an encoding of LK+(T) back into the more restrictive system LK(T). We then prove completeness of LKp(T) (and therefore of LK+(T)) with respect to first-order reasoning modulo the ground propositional lemmas of the background theory T .
            """ ;
    dct:identifier "hal-00779199" ;
    dct:issued "2026-05-09T17:29:03.064492"^^xsd:dateTime ;
    dct:language "en" ;
    dct:modified "2026-05-09T17:29:03.064498"^^xsd:dateTime ;
    dct:publisher <https://rec.harvest-normandie.data4citizen.com/organization/cce9db95-46d9-4dc2-84b6-764215d0a002> ;
    dct:title "Sequent Calculi with procedure calls" ;
    dcat:contactPoint [ a vcard:Organization ;
            vcard:fn "CCSD" ] ;
    dcat:distribution <https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-hal-00779199v4/resource/c1cfd78e-bc43-4d01-9336-12db204057a8> ;
    dcat:keyword "completeness",
        "cut-elimination",
        "focusing",
        "infoeu-reposemanticsreport",
        "infoinfo-locomputer-science-cslogic-in-computer-science-cslo",
        "polarities",
        "reports",
        "sequent-calculus" ;
    dcat:landingPage <https://hal.science/hal-00779199> .

<https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-hal-00779199v4/resource/c1cfd78e-bc43-4d01-9336-12db204057a8> a dcat:Distribution ;
    dct:format "HTML" ;
    dct:issued "2026-05-09T17:29:03.071964"^^xsd:dateTime ;
    dct:modified "2026-05-09T17:29:03.050647"^^xsd:dateTime ;
    dct:title "Sequent Calculi with procedure calls" ;
    dcat:accessURL <https://hal.science/hal-00779199> .

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

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