@inproceedings{10.1007/3-540-69778-0_29,
    Abstract = {We present two constructive proofs of the decidability of intuitionistic propositional logic by simultaneously constructing either a counter-model or a derivation. From these proofs, we extract two programs which have a sequent as input and return a derivation or a counter-model. The search tree of these algorithms is linearly bounded by the number of connectives of the input. Soundness of these programs follows from giving a correct construction of the derivations, similarly to Hudelmaier's work [7]; completeness from giving a correct construction of the counter-models, inspired by Miglioli, Moscato, and Ornaghi [8].},
    Address = {Berlin, Heidelberg},
    Author = {Weich, Klaus},
    BookTitle = {Automated Reasoning with Analytic Tableaux and Related Methods},
    Editor = {de Swart, Harrie},
    File = {Decision Procedures for Intuitionistic Propositional Logic by Program Extraction - Weich1998\_Chapter\_DecisionProceduresForIntuition - a - b.pdf},
    ISBN = {978-3-540-69778-7},
    Pages = {292--306},
    Publisher = {Springer Berlin Heidelberg},
    Title = {Decision Procedures for Intuitionistic Propositional Logic by Program Extraction},
    Year = {1998},
    date-added = {2020-09-23 11:16:57 +0200},
    date-modified = {2020-09-23 11:16:57 +0200},
    doi = {10.1007/3-540-69778-0_29}
}

@inproceedings{10.1007/3-540-69778-0_29, Abstract = {We present two constructive proofs of the decidability of intuitionistic propositional logic by simultaneously constructing either a counter-model or a derivation. From these proofs, we extract two programs which have a sequent as input and return a derivation or a counter-model. The search tree of these algorithms is linearly bounded by the number of connectives of the input. Soundness of these programs follows from giving a correct construction of the derivations, similarly to Hudelmaier's work [7]; completeness from giving a correct construction of the counter-models, inspired by Miglioli, Moscato, and Ornaghi [8].}, Address = {Berlin, Heidelberg}, Author = {Weich, Klaus}, BookTitle = {Automated Reasoning with Analytic Tableaux and Related Methods}, Editor = {de Swart, Harrie}, File = {Decision Procedures for Intuitionistic Propositional Logic by Program Extraction - Weich1998_Chapter_DecisionProceduresForIntuition - a - b.pdf}, ISBN = {978-3-540-69778-7}, Pages = {292--306}, Publisher = {Springer Berlin Heidelberg}, Title = {Decision Procedures for Intuitionistic Propositional Logic by Program Extraction}, Year = {1998}, date-added = {2020-09-23 11:16:57 +0200}, date-modified = {2020-09-23 11:16:57 +0200}, doi = {10.1007/3-540-69778-0_29} }