Refactor UI: Remove LogicBench tab, adapt Proof tab for external JSON

app.py

@@ -2,7 +2,7 @@
 Gradio application for SFOSR (Semantic Formal Ontology Structure Representation) System.
 
 Provides an interface to analyze, verify, and construct proofs using the SFOSR framework.
-Includes a tab for integrating with LogicBench tasks (requires LLM for text-to-SFOSR conversion).
+Users can input SFOSR JSON directly or use the proof tab with JSON generated externally (e.g., from LogicBench tasks via LLM).
 """
 
 import gradio as gr
@@ -110,6 +110,10 @@ def run_proof_construction(input_json_str, source_concept, target_concept):
         return "Source and Target concepts cannot be empty.", ""
 
     # Add the proof query to the input data
+    # If input_data doesn't exist yet (e.g., empty string), create it.
+    if input_data is None: 
+        input_data = {}
+        
     input_data["proof_query"] = {
         "source": source_concept,
         "target": target_concept
@@ -139,72 +143,6 @@ def run_proof_construction(input_json_str, source_concept, target_concept):
         print(f"Error during SFOSR proof: {e}\n{error_trace}") # Log for debugging
         return f"An error occurred: {e}", ""
 
-# --- Placeholder for LogicBench Integration --- 
-def run_logicbench_task(logicbench_context, logicbench_question):
-    """Placeholder function for LogicBench task processing."""
-    print(f"Received LogicBench Context: {logicbench_context[:100]}...")
-    print(f"Received LogicBench Question: {logicbench_question}")
-
-    # --- Stage 1: Text-to-SFOSR Conversion (using LLM - TO BE IMPLEMENTED) ---
-    generated_sfosr_json = {
-        "text": logicbench_context,
-        "vectors": [
-            {"id": "placeholder", "source": "PlaceholderSource", "target": "PlaceholderTarget", 
-             "type": "PlaceholderType", "axis": "placeholder", "justification": "LLM Step Not Implemented"}
-        ]
-    }
-    generated_sfosr_str = json.dumps(generated_sfosr_json, indent=2, ensure_ascii=False)
-
-    # --- Stage 2: SFOSR Processing (using the generated JSON) ---
-    if sfosr_instance is None:
-        final_answer = "Error: SFOSR System not available."
-        sfosr_proof_status = ""
-        sfosr_proof_details = ""
-    else:
-        try:
-            # Determine source/target for proof based on the question (requires logic)
-            # For now, let's use placeholder source/target from the generated JSON
-            # This part needs significant refinement based on how questions are mapped
-            source_concept_lb = generated_sfosr_json["vectors"][0]["source"]
-            target_concept_lb = generated_sfosr_json["vectors"][0]["target"]
-            
-            logicbench_input_data = generated_sfosr_json
-            logicbench_input_data["proof_query"] = {
-                "source": source_concept_lb,
-                "target": target_concept_lb 
-            }
-            
-            # Call the main process method
-            sfosr_result = sfosr_instance.process(logicbench_input_data)
-            sfosr_proof_result = sfosr_result.get("proof")
-
-            # --- Stage 3: Interpret SFOSR Result as LogicBench Answer (TO BE IMPLEMENTED) ---
-            if sfosr_proof_result and sfosr_proof_result.get("is_valid"):
-                final_answer = "Answer: Yes (Placeholder - based on successful SFOSR proof)"
-            else:
-                final_answer = "Answer: No/Unknown (Placeholder - SFOSR proof failed or invalid)"
-            
-            # Format proof output for display
-            if sfosr_proof_result:
-                 sfosr_proof_status = f"**Proof Status:** {sfosr_proof_result.get('status', 'N/A')}\n" \
-                                      f"**Is Valid:** {sfosr_proof_result.get('is_valid', 'N/A')}"
-                 if sfosr_proof_result.get('reason'):
-                      sfosr_proof_status += f"\n**Reason:** {sfosr_proof_result.get('reason')}"
-                 sfosr_proof_details = sfosr_proof_result
-            else:
-                sfosr_proof_status = "SFOSR Proof was not generated or failed."
-                sfosr_proof_details = {}
-                
-        except Exception as e:
-            error_trace = traceback.format_exc()
-            print(f"Error during LogicBench task processing: {e}\n{error_trace}")
-            final_answer = f"Error processing task: {e}"
-            sfosr_proof_status = "Error during processing"
-            sfosr_proof_details = {}
-
-    return final_answer, generated_sfosr_str, sfosr_proof_status, sfosr_proof_details
-
-
 # --- Example Input Formats ---
 example_verify_json = '''{
   "text": "Загрязнение воздуха вызывает респираторные заболевания. Загрязнение происходит из-за выбросов заводов.",
@@ -228,30 +166,31 @@ example_verify_json = '''{
   ]
 }'''
 
-example_proof_json = '''{
+# Example JSON potentially generated from LogicBench task: "If it rains, the ground gets wet. The ground is not wet. Question: Did it rain?"
+# We might want to prove: Rain -> False or check consistency
+example_logicbench_proof_json = '''{
   "vectors": [
     {
-      "id": "V1",
-      "source": "ВыбросыЗаводов",
-      "target": "ЗагрязнениеВоздуха",
-      "type": "Causality",
-      "axis": "relationship",
-      "justification": "Промышленные выбросы содержат вредные вещества."
+      "id": "LB1",
+      "source": "Rain",
+      "target": "GroundWet",
+      "type": "Implication",
+      "axis": "logic",
+      "justification": "If it rains, the ground gets wet."
     },
     {
-      "id": "V2",
-      "source": "ЗагрязнениеВоздуха",
-      "target": "РеспираторныеЗаболевания",
-      "type": "Causality",
-      "axis": "relationship",
-      "justification": "Вредные частицы попадают в дыхательную систему."
+      "id": "LB2",
+      "source": "GroundWet",
+      "target": "False",
+      "type": "IsA", 
+      "axis": "logic",
+      "justification": "The ground is not wet."
     }
   ]
 }'''
+example_logicbench_source = "Rain"
+example_logicbench_target = "False" # Target to prove based on the question "Did it rain?"
 
-# Example for LogicBench (replace with actual examples)
-example_logicbench_context = "If it rains, the ground gets wet. The ground is not wet."
-example_logicbench_question = "Did it rain?"
 
 # --- Gradio Interface Definition ---
 
@@ -333,41 +272,46 @@ with gr.Blocks(theme=gr.themes.Soft()) as demo:
                 label="Примеры входных данных"
             )
 
-        with gr.TabItem("Построение Доказательств"):
+        with gr.TabItem("Построение Доказательств / Задачи Логики"):
             gr.Markdown(
                 """
                 ### Как пользоваться:
                 
-                1. **Введите JSON** с векторами-посылками (см. пример)
-                2. **Укажите исходный концепт** (от которого начинается доказательство)
-                3. **Укажите целевой концепт** (к которому нужно построить доказательство)
-                4. **Нажмите кнопку** "Найти Доказательство"
-                5. **Посмотрите результат** справа - система попытается найти цепочку рассуждений
+                1. **Подготовьте SFOSR JSON:** 
+                   - Для обычных задач: Создайте JSON с векторами-посылками.
+                   - Для задач типа LogicBench: Используйте внешнюю LLM (например, спросите в чате), чтобы преобразовать текстовый контекст задачи в SFOSR JSON формат.
+                2. **Вставьте JSON** с векторами в поле ниже.
+                3. **Определите цель доказательства:** Исходя из вопроса задачи, определите, какую связь между концептами нужно доказать. 
+                   Например, для вопроса "Идет ли дождь?" и контекста "Если идет дождь, земля мокрая. Земля сухая.", 
+                   возможно, нужно доказать связь от "Rain" к "False".
+                4. **Укажите Исходный и Целевой концепты** в соответствующие поля.
+                5. **Нажмите кнопку** "Найти Доказательство".
+                6. **Интерпретируйте результат:** Успешное доказательство (Valid: True) или его отсутствие поможет ответить на исходный вопрос задачи.
                 
                 #### Что такое доказательство?
                 Доказательство - это цепочка логических шагов, которая показывает, как от исходного концепта можно
                 прийти к целевому, используя имеющиеся векторы и правила вывода. Например, если у вас есть
-                векторы "A вызывает B" и "B вызывает C", система может вывести "A вызывает C".
+                векторы "A → B" и "B → C", система может вывести "A → C".
                 """
             )
             with gr.Row():
                 with gr.Column(scale=1):
                     gr.Markdown("### Входные Данные и Запрос")
                     input_json_p = gr.Textbox(
-                        lines=10,
+                        lines=15, # Increased lines for potentially larger JSON
                         label="SFOSR JSON с Векторами",
-                        info="Введите JSON с векторами, которые будут использованы как посылки для доказательства",
-                        placeholder='{\n  "vectors": [\n    {\n      "id": "V1", "source": "ВыбросыЗаводов", "target": "ЗагрязнениеВоздуха", "type": "Causality", "axis": "relationship" \n    },\n    {\n      "id": "V2", "source": "ЗагрязнениеВоздуха", "target": "РеспираторныеЗаболевания", "type": "Causality", "axis": "relationship" \n    }\n  ]\n}'
+                        info="Введите JSON с векторами, которые будут использованы как посылки для доказательства (можно сгенерировать из текста через LLM)",
+                        placeholder='{\n  "vectors": [\n    {\n      "id": "V1", "source": "КонцептА", "target": "КонцептБ", "type": "Implication", "axis": "logic" \n    }\n    // ... другие векторы ...\n  ]\n}'
                     )
                     source_concept_input = gr.Textbox(
                         label="Исходный Концепт", 
                         info="Введите имя концепта, от которого начинается доказательство",
-                        placeholder="ВыбросыЗаводов"
+                        placeholder="Например: Rain"
                     )
                     target_concept_input = gr.Textbox(
                         label="Целевой Концепт", 
                         info="Введите имя концепта, к которому нужно построить доказательство",
-                        placeholder="РеспираторныеЗаболевания"
+                        placeholder="Например: False"
                     )
                     p_button = gr.Button("Найти Доказательство", variant="primary")
                 with gr.Column(scale=1):
@@ -378,63 +322,13 @@ with gr.Blocks(theme=gr.themes.Soft()) as demo:
 
             gr.Examples(
                 examples=[
-                    [example_proof_json, "ВыбросыЗаводов", "РеспираторныеЗаболевания"]
+                    # Example with manually created proof vectors
+                    # [example_proof_json, "ВыбросыЗаводов", "РеспираторныеЗаболевания"],
+                    # Example potentially derived from LogicBench task
+                    [example_logicbench_proof_json, example_logicbench_source, example_logicbench_target]
                 ],
                 inputs=[input_json_p, source_concept_input, target_concept_input],
-                label="Пример построения доказательства"
-            )
-
-        with gr.TabItem("Интеграция с LogicBench"):
-             gr.Markdown(
-                """
-                ### Решение Задач LogicBench (Экспериментально)
-                
-                Эта вкладка демонстрирует гибридный подход: 
-                1. **LLM** преобразует текстовую задачу из LogicBench в структурированные SFOSR векторы (JSON).
-                2. **SFOSR** система анализирует и пытается доказать ответ на вопрос задачи, используя сгенерированные векторы.
-                
-                **Внимание:** Шаг 1 (LLM преобразование) еще не реализован. Сейчас используется placeholder.
-                
-                #### Как пользоваться (когда будет реализовано):
-                1. Вставьте **Контекст/Посылки** из задачи LogicBench.
-                2. Вставьте **Вопрос** из задачи LogicBench.
-                3. Нажмите кнопку "Решить Задачу LogicBench".
-                4. Посмотрите **Финальный Ответ** и детали работы SFOSR.
-                """
-            )
-             with gr.Row():
-                with gr.Column(scale=1):
-                    gr.Markdown("### Входные данные из LogicBench")
-                    lb_context_input = gr.Textbox(
-                        lines=10,
-                        label="Контекст / Посылки",
-                        info="Вставьте текст контекста или посылок из задачи LogicBench",
-                        placeholder="Пример: Если идет дождь, трава мокрая. Трава сухая."
-                    )
-                    lb_question_input = gr.Textbox(
-                        lines=2,
-                        label="Вопрос",
-                        info="Вставьте вопрос из задачи LogicBench",
-                        placeholder="Пример: Идет ли дождь?"
-                    )
-                    lb_button = gr.Button("Решить Задачу LogicBench", variant="primary")
-                
-                with gr.Column(scale=1):
-                    gr.Markdown("### Результат Решения")
-                    lb_final_answer_output = gr.Markdown(label="Финальный Ответ")
-                    with gr.Accordion("Детали Обработки SFOSR", open=False):
-                        gr.Markdown("#### Сгенерированный SFOSR JSON (LLM Шаг - Placeholder)")
-                        lb_sfosr_json_output = gr.Code(language="json", label="SFOSR JSON")
-                        gr.Markdown("#### Результат Доказательства SFOSR")
-                        lb_proof_status_output = gr.Markdown(label="Статус Доказательства SFOSR")
-                        lb_proof_details_output = gr.JSON(label="Структура Доказательства SFOSR")
-
-             gr.Examples(
-                 examples=[
-                     [example_logicbench_context, example_logicbench_question]
-                 ],
-                 inputs=[lb_context_input, lb_question_input],
-                 label="Пример Задачи LogicBench"
+                label="Примеры для Построения Доказательств"
             )
 
         with gr.TabItem("Справка"):
@@ -504,12 +398,7 @@ with gr.Blocks(theme=gr.themes.Soft()) as demo:
             outputs=[proof_status_output, proof_details_output]
         )
         
-        # LogicBench Integration Tab
-        lb_button.click(
-            fn=run_logicbench_task, 
-            inputs=[lb_context_input, lb_question_input],
-            outputs=[lb_final_answer_output, lb_sfosr_json_output, lb_proof_status_output, lb_proof_details_output]
-        )
+        # REMOVED LogicBench Integration Tab Handler
         
     else:
          # Display a persistent error if the system couldn't load