{"id":"W2620945766","doi":"","title":"Proof-search and countermodel generation in propositional BI Logic - extended abstract -","year":2001,"lang":"en","type":"article","venue":"","topic":"Semantic Web and Ontologies","field":"Computer Science","cited_by":7,"is_retracted":false,"has_abstract":true,"ca_institutions":"Prevention of Organ Failure","funders":"","keywords":"Intuitionistic logic; Intermediate logic; Kripke semantics; Linear logic; Zeroth-order logic; Sequent calculus; Monoid; Autoepistemic logic; Computer science; Well-formed formula; Propositional variable; Semantics (computer science); Interpretation (philosophy); Dynamic logic (digital electronics); Structural proof theory; Kripke structure; Proof theory; Theoretical computer science; Mathematics; Discrete mathematics; Description logic; Programming language; Multimodal logic; Model checking; Mathematical proof","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0001940735,0.00006347711,0.0000705034,0.00007769901,0.00005318872,0.0001251125,0.0001791611,0.00003886006,0.00003433666],"category_scores_gemma":[0.000009495846,0.00004762777,0.00001180197,0.0001104806,0.00003825205,0.0003759267,0.00006723136,0.00006306957,0.00001236875],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002221717,"about_ca_system_score_gemma":0.00004593141,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00009723417,"about_ca_topic_score_gemma":0.0001756023,"domain_scores_codex":[0.9993083,0.00001852394,0.0001200815,0.0002301743,0.000166132,0.0001567518],"domain_scores_gemma":[0.9997576,0.00002015992,0.000013346,0.0001413212,0.00003881662,0.00002878332],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00004791653,0.0007855547,0.0155418,0.00004805518,0.00002075159,0.0004346089,0.001333638,0.003263847,0.02924024,0.7611561,0.00157594,0.1865515],"study_design_scores_gemma":[0.0003382544,0.00008401689,0.1476076,0.000007556212,0.00000105025,0.0001196792,0.00003208674,0.8345552,0.002938475,0.01409836,0.00008779591,0.0001299206],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.6926729,0.0001362893,0.2983848,0.002314727,0.00006586647,0.0001898841,4.518239e-7,0.00006615907,0.006168964],"genre_scores_gemma":[0.9795519,0.00002616705,0.01981255,0.0002852133,0.00003619133,0.00001110879,0.000003371405,0.000001867748,0.0002715931],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.8312913,"threshold_uncertainty_score":0.1942204,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06139524417993749,"score_gpt":0.3023926488246079,"score_spread":0.2409974046446704,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}