reasonkit/thinktool/modules/

laserlogic.rs

//! # LaserLogic Module - Precision Deductive Reasoning
//!
//! Performs rigorous logical analysis with:
//! - First-order logic (FOL) translation and validation
//! - Formal fallacy detection (10+ types)
//! - Argument structure validation
//! - Syllogism analysis
//! - Contradiction detection
//!
//! ## Scientific Foundation
//!
//! Based on classical deductive logic and NL2FOL research:
//! - Modus ponens, modus tollens, hypothetical syllogism
//! - 78-80% F1 on fallacy detection with FOL translation
//! - Formal verification through constraint satisfaction
//!
//! ## Usage
//!
//! ```rust,ignore
//! use reasonkit::thinktool::modules::{LaserLogic, LaserLogicConfig};
//!
//! // Quick validation
//! let laser = LaserLogic::new();
//! let result = laser.analyze_argument(
//!     &["All humans are mortal", "Socrates is human"],
//!     "Socrates is mortal"
//! )?;
//!
//! // With custom configuration
//! let laser = LaserLogic::with_config(LaserLogicConfig {
//!     detect_fallacies: true,
//!     check_validity: true,
//!     check_soundness: true,
//!     max_premise_depth: 10,
//!     ..Default::default()
//! });
//! ```

use super::{ThinkToolContext, ThinkToolModule, ThinkToolModuleConfig, ThinkToolOutput};
use crate::error::{Error, Result};
use serde::{Deserialize, Serialize};
use std::collections::HashSet;

// =============================================================================
// Configuration
// =============================================================================

/// Configuration for LaserLogic analysis depth and features
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct LaserLogicConfig {
    /// Enable fallacy detection
    pub detect_fallacies: bool,
    /// Enable validity checking (conclusion follows from premises)
    pub check_validity: bool,
    /// Enable soundness checking (valid + true premises)
    pub check_soundness: bool,
    /// Maximum number of premises to analyze
    pub max_premise_depth: usize,
    /// Enable syllogism detection and analysis
    pub analyze_syllogisms: bool,
    /// Enable contradiction detection
    pub detect_contradictions: bool,
    /// Minimum confidence threshold for conclusions
    pub confidence_threshold: f64,
    /// Enable verbose output with reasoning steps
    pub verbose_output: bool,
}

impl Default for LaserLogicConfig {
    fn default() -> Self {
        Self {
            detect_fallacies: true,
            check_validity: true,
            check_soundness: true,
            max_premise_depth: 10,
            analyze_syllogisms: true,
            detect_contradictions: true,
            confidence_threshold: 0.7,
            verbose_output: false,
        }
    }
}

impl LaserLogicConfig {
    /// Quick check mode - validity and basic fallacy detection only
    pub fn quick() -> Self {
        Self {
            detect_fallacies: true,
            check_validity: true,
            check_soundness: false,
            max_premise_depth: 5,
            analyze_syllogisms: false,
            detect_contradictions: false,
            confidence_threshold: 0.6,
            verbose_output: false,
        }
    }

    /// Deep analysis mode - all features enabled
    pub fn deep() -> Self {
        Self {
            detect_fallacies: true,
            check_validity: true,
            check_soundness: true,
            max_premise_depth: 20,
            analyze_syllogisms: true,
            detect_contradictions: true,
            confidence_threshold: 0.8,
            verbose_output: true,
        }
    }

    /// Paranoid mode - strictest validation
    pub fn paranoid() -> Self {
        Self {
            detect_fallacies: true,
            check_validity: true,
            check_soundness: true,
            max_premise_depth: 50,
            analyze_syllogisms: true,
            detect_contradictions: true,
            confidence_threshold: 0.9,
            verbose_output: true,
        }
    }
}

// =============================================================================
// Logical Structures
// =============================================================================

/// A logical argument with premises and conclusion
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct Argument {
    /// The premises (supporting statements)
    pub premises: Vec<Premise>,
    /// The conclusion being argued
    pub conclusion: String,
    /// Argument form (modus ponens, syllogism, etc.)
    pub form: Option<ArgumentForm>,
}

impl Argument {
    /// Create a new argument from premises and conclusion
    pub fn new(premises: Vec<&str>, conclusion: &str) -> Self {
        Self {
            premises: premises.iter().map(|p| Premise::new(p)).collect(),
            conclusion: conclusion.to_string(),
            form: None,
        }
    }

    /// Create with typed premises
    pub fn with_premises(premises: Vec<Premise>, conclusion: &str) -> Self {
        Self {
            premises,
            conclusion: conclusion.to_string(),
            form: None,
        }
    }
}

/// A single premise in an argument
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct Premise {
    /// The premise statement
    pub statement: String,
    /// Premise type (universal, particular, conditional)
    pub premise_type: PremiseType,
    /// Confidence in the premise truth (0.0 - 1.0)
    pub confidence: f64,
    /// Evidence supporting this premise
    pub evidence: Vec<String>,
}

impl Premise {
    /// Create a new premise
    pub fn new(statement: &str) -> Self {
        let premise_type = Self::infer_type(statement);
        Self {
            statement: statement.to_string(),
            premise_type,
            confidence: 1.0,
            evidence: Vec::new(),
        }
    }

    /// Create with explicit type and confidence
    pub fn with_type(statement: &str, premise_type: PremiseType, confidence: f64) -> Self {
        Self {
            statement: statement.to_string(),
            premise_type,
            confidence,
            evidence: Vec::new(),
        }
    }

    /// Infer premise type from statement
    fn infer_type(statement: &str) -> PremiseType {
        let lower = statement.to_lowercase();

        // Universal quantifiers
        if lower.starts_with("all ")
            || lower.starts_with("every ")
            || lower.starts_with("each ")
            || lower.contains(" always ")
            || lower.starts_with("no ")
        {
            return PremiseType::Universal;
        }

        // Particular quantifiers
        if lower.starts_with("some ")
            || lower.starts_with("most ")
            || lower.starts_with("many ")
            || lower.starts_with("few ")
            || lower.contains(" sometimes ")
        {
            return PremiseType::Particular;
        }

        // Conditional
        if lower.starts_with("if ")
            || lower.contains(" then ")
            || lower.contains(" implies ")
            || lower.contains(" only if ")
        {
            return PremiseType::Conditional;
        }

        // Disjunctive
        if lower.contains(" or ") || lower.starts_with("either ") {
            return PremiseType::Disjunctive;
        }

        // Negative
        if lower.starts_with("not ") || lower.contains(" not ") || lower.starts_with("no ") {
            return PremiseType::Negative;
        }

        // Default to singular
        PremiseType::Singular
    }

    /// Add evidence for this premise
    pub fn with_evidence(mut self, evidence: &str) -> Self {
        self.evidence.push(evidence.to_string());
        self
    }
}

/// Types of premises in logical arguments
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum PremiseType {
    /// Universal (All X are Y)
    Universal,
    /// Particular (Some X are Y)
    Particular,
    /// Singular (X is Y)
    Singular,
    /// Conditional (If X then Y)
    Conditional,
    /// Disjunctive (X or Y)
    Disjunctive,
    /// Negative (X is not Y)
    Negative,
}

/// Common argument forms
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum ArgumentForm {
    /// Modus Ponens: P->Q, P |- Q
    ModusPonens,
    /// Modus Tollens: P->Q, ~Q |- ~P
    ModusTollens,
    /// Hypothetical Syllogism: P->Q, Q->R |- P->R
    HypotheticalSyllogism,
    /// Disjunctive Syllogism: P v Q, ~P |- Q
    DisjunctiveSyllogism,
    /// Categorical Syllogism: All M are P, All S are M |- All S are P
    CategoricalSyllogism,
    /// Constructive Dilemma: (P->Q) ^ (R->S), P v R |- Q v S
    ConstructiveDilemma,
    /// Destructive Dilemma: (P->Q) ^ (R->S), ~Q v ~S |- ~P v ~R
    DestructiveDilemma,
    /// Reductio Ad Absurdum (proof by contradiction)
    ReductioAdAbsurdum,
    /// Unknown or complex form
    Unknown,
}

impl ArgumentForm {
    /// Get the description of this argument form
    pub fn description(&self) -> &'static str {
        match self {
            Self::ModusPonens => "Modus Ponens (affirming the antecedent)",
            Self::ModusTollens => "Modus Tollens (denying the consequent)",
            Self::HypotheticalSyllogism => "Hypothetical Syllogism (chain reasoning)",
            Self::DisjunctiveSyllogism => "Disjunctive Syllogism (process of elimination)",
            Self::CategoricalSyllogism => "Categorical Syllogism (term-based reasoning)",
            Self::ConstructiveDilemma => "Constructive Dilemma (complex conditional)",
            Self::DestructiveDilemma => "Destructive Dilemma (complex conditional)",
            Self::ReductioAdAbsurdum => "Reductio Ad Absurdum (proof by contradiction)",
            Self::Unknown => "Unknown or complex argument form",
        }
    }

    /// Check if this form is always valid
    pub fn is_valid_form(&self) -> bool {
        !matches!(self, Self::Unknown)
    }
}

// =============================================================================
// Fallacy Types
// =============================================================================

/// Logical fallacies detectable by LaserLogic
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub enum Fallacy {
    // Formal Fallacies (invalid argument structure)
    /// Affirming the Consequent: P->Q, Q |- P (INVALID)
    AffirmingConsequent,
    /// Denying the Antecedent: P->Q, ~P |- ~Q (INVALID)
    DenyingAntecedent,
    /// Undistributed Middle: All A are B, All C are B |- All A are C (INVALID)
    UndistributedMiddle,
    /// Illicit Major: Distribution error in major term
    IllicitMajor,
    /// Illicit Minor: Distribution error in minor term
    IllicitMinor,
    /// Four-Term Fallacy: Equivocation in syllogism
    FourTerms,
    /// Existential Fallacy: Assuming existence from universal
    ExistentialFallacy,
    /// Affirming a Disjunct: P v Q, P |- ~Q (INVALID for inclusive or)
    AffirmingDisjunct,

    // Semi-Formal Fallacies
    /// Circular Reasoning: Conclusion appears in premises
    CircularReasoning,
    /// Non Sequitur: Conclusion doesn't follow
    NonSequitur,
    /// Composition: Parts to whole error
    Composition,
    /// Division: Whole to parts error
    Division,

    // Causal Fallacies
    /// Post Hoc: A then B, therefore A caused B
    PostHoc,
    /// Slippery Slope: Unwarranted chain of consequences
    SlipperySlope,
    /// False Cause: Incorrectly identifying causation
    FalseCause,

    // Relevance Fallacies (informal but detectable through structure)
    /// Straw Man: Misrepresenting the argument
    StrawMan,
    /// False Dichotomy: Only two options when more exist
    FalseDichotomy,
    /// Equivocation: Using term with different meanings
    Equivocation,
}

impl Fallacy {
    /// Get a description of this fallacy
    pub fn description(&self) -> &'static str {
        match self {
            Self::AffirmingConsequent => {
                "Inferring P from P->Q and Q. Just because the outcome occurred doesn't mean the specific cause happened."
            }
            Self::DenyingAntecedent => {
                "Inferring ~Q from P->Q and ~P. The consequent might be true for other reasons."
            }
            Self::UndistributedMiddle => {
                "The middle term is not distributed in at least one premise of the syllogism."
            }
            Self::IllicitMajor => {
                "The major term is distributed in the conclusion but not in the major premise."
            }
            Self::IllicitMinor => {
                "The minor term is distributed in the conclusion but not in the minor premise."
            }
            Self::FourTerms => {
                "Four distinct terms used where a syllogism requires exactly three."
            }
            Self::ExistentialFallacy => {
                "Drawing an existential conclusion from purely universal premises."
            }
            Self::AffirmingDisjunct => {
                "Concluding ~Q from (P v Q) and P. With inclusive OR, both can be true."
            }
            Self::CircularReasoning => {
                "The conclusion is essentially restated in the premises."
            }
            Self::NonSequitur => {
                "The conclusion does not logically follow from the premises."
            }
            Self::Composition => {
                "Assuming what's true of parts must be true of the whole."
            }
            Self::Division => {
                "Assuming what's true of the whole must be true of the parts."
            }
            Self::PostHoc => {
                "Assuming A caused B simply because A preceded B."
            }
            Self::SlipperySlope => {
                "Claiming that one event will inevitably lead to a chain of negative events."
            }
            Self::FalseCause => {
                "Incorrectly identifying something as the cause."
            }
            Self::StrawMan => {
                "Misrepresenting someone's argument to make it easier to attack."
            }
            Self::FalseDichotomy => {
                "Presenting only two options when more exist."
            }
            Self::Equivocation => {
                "Using the same term with different meanings in different parts of the argument."
            }
        }
    }

    /// Get the logical pattern of this fallacy
    pub fn pattern(&self) -> &'static str {
        match self {
            Self::AffirmingConsequent => "P->Q, Q |- P (INVALID)",
            Self::DenyingAntecedent => "P->Q, ~P |- ~Q (INVALID)",
            Self::UndistributedMiddle => "All A are B, All C are B |- All A are C (INVALID)",
            Self::IllicitMajor => "Major term undistributed in premise, distributed in conclusion",
            Self::IllicitMinor => "Minor term undistributed in premise, distributed in conclusion",
            Self::FourTerms => "A-B, C-D |- invalid (4 terms, not 3)",
            Self::ExistentialFallacy => "All P are Q |- Some P are Q (INVALID if no P exist)",
            Self::AffirmingDisjunct => "P v Q, P |- ~Q (INVALID for inclusive or)",
            Self::CircularReasoning => "P |- P (trivially valid but uninformative)",
            Self::NonSequitur => "Premises do not entail conclusion",
            Self::Composition => "Part(x) is P |- Whole(x) is P (INVALID)",
            Self::Division => "Whole(x) is P |- Part(x) is P (INVALID)",
            Self::PostHoc => "A then B |- A caused B (INVALID)",
            Self::SlipperySlope => "A -> B -> C -> ... -> Z (chain not established)",
            Self::FalseCause => "Correlation or sequence |- Causation (INVALID)",
            Self::StrawMan => "Argument(A') attacked instead of Argument(A)",
            Self::FalseDichotomy => "P v Q presented where P v Q v R v ... exists",
            Self::Equivocation => "Term T used as T1 and T2 (different meanings)",
        }
    }

    /// Get severity (1-5, where 5 is most severe)
    pub fn severity(&self) -> u8 {
        match self {
            Self::AffirmingConsequent | Self::DenyingAntecedent => 5,
            Self::UndistributedMiddle | Self::IllicitMajor | Self::IllicitMinor => 5,
            Self::FourTerms | Self::ExistentialFallacy => 4,
            Self::CircularReasoning | Self::NonSequitur => 5,
            Self::Composition | Self::Division => 3,
            Self::PostHoc | Self::FalseCause | Self::SlipperySlope => 4,
            Self::StrawMan | Self::FalseDichotomy | Self::Equivocation => 4,
            Self::AffirmingDisjunct => 4,
        }
    }

    /// Is this a formal (structural) fallacy?
    pub fn is_formal(&self) -> bool {
        matches!(
            self,
            Self::AffirmingConsequent
                | Self::DenyingAntecedent
                | Self::UndistributedMiddle
                | Self::IllicitMajor
                | Self::IllicitMinor
                | Self::FourTerms
                | Self::ExistentialFallacy
                | Self::AffirmingDisjunct
        )
    }
}

/// A detected fallacy with evidence
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct DetectedFallacy {
    /// The type of fallacy detected
    pub fallacy: Fallacy,
    /// Confidence in the detection (0.0 - 1.0)
    pub confidence: f64,
    /// Evidence explaining why this is a fallacy
    pub evidence: String,
    /// Which premises are involved (indices)
    pub involved_premises: Vec<usize>,
    /// Suggested fix
    pub suggestion: String,
}

impl DetectedFallacy {
    /// Create a new detected fallacy
    pub fn new(fallacy: Fallacy, confidence: f64, evidence: &str) -> Self {
        Self {
            fallacy,
            confidence,
            evidence: evidence.to_string(),
            involved_premises: Vec::new(),
            suggestion: String::new(),
        }
    }

    /// Add involved premises
    pub fn with_premises(mut self, premises: Vec<usize>) -> Self {
        self.involved_premises = premises;
        self
    }

    /// Add a suggestion for fixing
    pub fn with_suggestion(mut self, suggestion: &str) -> Self {
        self.suggestion = suggestion.to_string();
        self
    }
}

// =============================================================================
// Analysis Results
// =============================================================================

/// Validity status of an argument
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum ValidityStatus {
    /// Argument is logically valid (conclusion follows from premises)
    Valid,
    /// Argument is logically invalid (conclusion does not follow)
    Invalid,
    /// Validity could not be determined
    Undetermined,
}

/// Soundness status of an argument
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum SoundnessStatus {
    /// Argument is sound (valid with true premises)
    Sound,
    /// Argument is unsound (invalid or false premises)
    Unsound,
    /// Soundness could not be determined
    Undetermined,
}

/// Complete analysis result from LaserLogic
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct LaserLogicResult {
    /// The argument that was analyzed
    pub argument: Argument,
    /// Validity status
    pub validity: ValidityStatus,
    /// Validity explanation
    pub validity_explanation: String,
    /// Soundness status
    pub soundness: SoundnessStatus,
    /// Soundness explanation
    pub soundness_explanation: String,
    /// Detected fallacies
    pub fallacies: Vec<DetectedFallacy>,
    /// Detected argument form
    pub argument_form: Option<ArgumentForm>,
    /// Overall confidence in the analysis (0.0 - 1.0)
    pub confidence: f64,
    /// Reasoning steps taken
    pub reasoning_steps: Vec<String>,
    /// Suggestions for improvement
    pub suggestions: Vec<String>,
    /// Detected contradictions
    pub contradictions: Vec<Contradiction>,
}

impl LaserLogicResult {
    /// Create a new result
    fn new(argument: Argument) -> Self {
        Self {
            argument,
            validity: ValidityStatus::Undetermined,
            validity_explanation: String::new(),
            soundness: SoundnessStatus::Undetermined,
            soundness_explanation: String::new(),
            fallacies: Vec::new(),
            argument_form: None,
            confidence: 0.0,
            reasoning_steps: Vec::new(),
            suggestions: Vec::new(),
            contradictions: Vec::new(),
        }
    }

    /// Get overall verdict
    pub fn verdict(&self) -> &'static str {
        match (self.validity, self.soundness) {
            (ValidityStatus::Valid, SoundnessStatus::Sound) => {
                "SOUND: Argument is valid with true premises"
            }
            (ValidityStatus::Valid, SoundnessStatus::Unsound) => {
                "VALID BUT UNSOUND: Logic correct, but premises questionable"
            }
            (ValidityStatus::Valid, SoundnessStatus::Undetermined) => {
                "VALID: Logic correct, premises unverified"
            }
            (ValidityStatus::Invalid, _) => "INVALID: Conclusion does not follow from premises",
            (ValidityStatus::Undetermined, _) => "UNDETERMINED: Could not fully analyze",
        }
    }

    /// Check if any fallacies were detected
    pub fn has_fallacies(&self) -> bool {
        !self.fallacies.is_empty()
    }

    /// Get the most severe fallacy
    pub fn most_severe_fallacy(&self) -> Option<&DetectedFallacy> {
        self.fallacies
            .iter()
            .max_by_key(|f| (f.fallacy.severity(), (f.confidence * 100.0) as u32))
    }

    /// Check if argument is logically valid
    pub fn is_valid(&self) -> bool {
        self.validity == ValidityStatus::Valid
    }

    /// Check if argument is sound
    pub fn is_sound(&self) -> bool {
        self.soundness == SoundnessStatus::Sound
    }
}

/// A detected contradiction between statements
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct Contradiction {
    /// First conflicting statement (premise index or "conclusion")
    pub statement_a: String,
    /// Second conflicting statement
    pub statement_b: String,
    /// Type of contradiction
    pub contradiction_type: ContradictionType,
    /// Explanation
    pub explanation: String,
}

/// Types of contradictions
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum ContradictionType {
    /// Direct negation (P and ~P)
    DirectNegation,
    /// Mutual exclusion (cannot both be true)
    MutualExclusion,
    /// Implicit contradiction (follows from premises)
    Implicit,
}

// =============================================================================
// LaserLogic Module Implementation
// =============================================================================

/// LaserLogic reasoning module for precision deductive analysis.
///
/// Provides formal logical analysis including:
/// - Argument structure validation
/// - Fallacy detection
/// - Validity and soundness checking
/// - Syllogism analysis
pub struct LaserLogic {
    /// Module configuration
    config: ThinkToolModuleConfig,
    /// Analysis configuration
    analysis_config: LaserLogicConfig,
}

impl Default for LaserLogic {
    fn default() -> Self {
        Self::new()
    }
}

impl LaserLogic {
    /// Create a new LaserLogic module with default configuration.
    pub fn new() -> Self {
        Self {
            config: ThinkToolModuleConfig {
                name: "LaserLogic".to_string(),
                version: "3.0.0".to_string(),
                description: "Precision deductive reasoning with fallacy detection".to_string(),
                confidence_weight: 0.25,
            },
            analysis_config: LaserLogicConfig::default(),
        }
    }

    /// Create with custom configuration
    pub fn with_config(analysis_config: LaserLogicConfig) -> Self {
        Self {
            config: ThinkToolModuleConfig {
                name: "LaserLogic".to_string(),
                version: "3.0.0".to_string(),
                description: "Precision deductive reasoning with fallacy detection".to_string(),
                confidence_weight: 0.25,
            },
            analysis_config,
        }
    }

    /// Get the analysis configuration
    pub fn analysis_config(&self) -> &LaserLogicConfig {
        &self.analysis_config
    }

    /// Analyze an argument given premises and conclusion
    pub fn analyze_argument(
        &self,
        premises: &[&str],
        conclusion: &str,
    ) -> Result<LaserLogicResult> {
        let argument = Argument::new(premises.to_vec(), conclusion);
        self.analyze(argument)
    }

    /// Analyze a structured argument
    pub fn analyze(&self, argument: Argument) -> Result<LaserLogicResult> {
        // Validate input
        if argument.premises.is_empty() {
            return Err(Error::validation("Argument must have at least one premise"));
        }

        if argument.premises.len() > self.analysis_config.max_premise_depth {
            return Err(Error::validation(format!(
                "Too many premises ({} > {})",
                argument.premises.len(),
                self.analysis_config.max_premise_depth
            )));
        }

        let mut result = LaserLogicResult::new(argument.clone());

        // Step 1: Detect argument form
        result
            .reasoning_steps
            .push("Step 1: Identifying argument form...".to_string());
        result.argument_form = self.detect_argument_form(&argument);
        if let Some(form) = result.argument_form {
            result
                .reasoning_steps
                .push(format!("  Detected: {}", form.description()));
        }

        // Step 2: Check validity
        if self.analysis_config.check_validity {
            result
                .reasoning_steps
                .push("Step 2: Checking logical validity...".to_string());
            let (validity, explanation) = self.check_validity(&argument);
            result.validity = validity;
            result.validity_explanation = explanation.clone();
            result.reasoning_steps.push(format!("  {}", explanation));
        }

        // Step 3: Detect fallacies
        if self.analysis_config.detect_fallacies {
            result
                .reasoning_steps
                .push("Step 3: Scanning for fallacies...".to_string());
            let fallacies = self.detect_fallacies(&argument);
            for fallacy in &fallacies {
                result.reasoning_steps.push(format!(
                    "  Found: {} (confidence: {:.2})",
                    fallacy.fallacy.description(),
                    fallacy.confidence
                ));
            }
            result.fallacies = fallacies;
        }

        // Step 4: Detect contradictions
        if self.analysis_config.detect_contradictions {
            result
                .reasoning_steps
                .push("Step 4: Checking for contradictions...".to_string());
            result.contradictions = self.detect_contradictions(&argument);
            if result.contradictions.is_empty() {
                result
                    .reasoning_steps
                    .push("  No contradictions found.".to_string());
            } else {
                for contradiction in &result.contradictions {
                    result.reasoning_steps.push(format!(
                        "  Contradiction: {} vs {} - {}",
                        contradiction.statement_a,
                        contradiction.statement_b,
                        contradiction.explanation
                    ));
                }
            }
        }

        // Step 5: Check soundness
        if self.analysis_config.check_soundness {
            result
                .reasoning_steps
                .push("Step 5: Evaluating soundness...".to_string());
            let (soundness, explanation) = self.check_soundness(&argument, result.validity);
            result.soundness = soundness;
            result.soundness_explanation = explanation.clone();
            result.reasoning_steps.push(format!("  {}", explanation));
        }

        // Calculate overall confidence
        result.confidence = self.calculate_confidence(&result);

        // Generate suggestions
        result.suggestions = self.generate_suggestions(&result);

        Ok(result)
    }

    /// Clean a logical term by removing punctuation and extra whitespace
    fn clean_term(term: &str) -> String {
        term.trim()
            .trim_matches(|c: char| c.is_ascii_punctuation())
            .trim()
            .to_string()
    }

    /// Detect the argument form
    fn detect_argument_form(&self, argument: &Argument) -> Option<ArgumentForm> {
        // Look for conditional patterns
        let has_conditional = argument
            .premises
            .iter()
            .any(|p| p.premise_type == PremiseType::Conditional);

        let has_disjunctive = argument
            .premises
            .iter()
            .any(|p| p.premise_type == PremiseType::Disjunctive);

        let has_universal = argument
            .premises
            .iter()
            .any(|p| p.premise_type == PremiseType::Universal);

        // Check for modus ponens pattern: P->Q, P |- Q
        if has_conditional && argument.premises.len() >= 2 {
            // Simplified detection - look for "if...then" followed by affirming antecedent
            let conditional = argument
                .premises
                .iter()
                .find(|p| p.premise_type == PremiseType::Conditional);

            if let Some(cond) = conditional {
                let cond_lower = cond.statement.to_lowercase();
                if cond_lower.starts_with("if ") {
                    // Extract antecedent (roughly)
                    if let Some(then_idx) = cond_lower.find(" then ") {
                        // Clean the antecedent by removing punctuation
                        let antecedent = Self::clean_term(&cond_lower[3..then_idx]);

                        // Check if another premise affirms the antecedent
                        let affirms_antecedent = argument.premises.iter().any(|p| {
                            let p_lower = p.statement.to_lowercase();
                            let p_clean = Self::clean_term(&p_lower);
                            p.premise_type != PremiseType::Conditional
                                && (p_clean == antecedent || p_clean.contains(&antecedent))
                        });

                        // Check if another premise denies the antecedent (potential fallacy)
                        let denies_antecedent = argument.premises.iter().any(|p| {
                            let p_lower = p.statement.to_lowercase();
                            (p_lower.contains("not ") || p_lower.starts_with("no "))
                                && p_lower.contains(&antecedent)
                        });

                        if affirms_antecedent {
                            return Some(ArgumentForm::ModusPonens);
                        }
                        if denies_antecedent {
                            // This would be denying the antecedent - but we return the form anyway
                            return Some(ArgumentForm::Unknown); // Fallacy pattern
                        }
                    }
                }
            }
        }

        // Check for disjunctive syllogism: P v Q, ~P |- Q
        if has_disjunctive && argument.premises.len() >= 2 {
            let has_negation = argument.premises.iter().any(|p| {
                p.premise_type == PremiseType::Negative
                    || p.statement.to_lowercase().contains("not ")
            });

            if has_negation {
                return Some(ArgumentForm::DisjunctiveSyllogism);
            }
        }

        // Check for categorical syllogism: All M are P, All S are M |- All S are P
        // Also handles mixed syllogisms with singular premises (e.g., Socratic syllogism)
        if has_universal && argument.premises.len() >= 2 {
            let universal_count = argument
                .premises
                .iter()
                .filter(|p| p.premise_type == PremiseType::Universal)
                .count();

            // Classic categorical syllogism requires 2 universal premises
            if universal_count >= 2 {
                return Some(ArgumentForm::CategoricalSyllogism);
            }

            // Mixed syllogism: 1 universal + 1 singular (e.g., "All humans are mortal" + "Socrates is human")
            // This is a valid syllogistic form (Barbara with singular minor)
            let singular_count = argument
                .premises
                .iter()
                .filter(|p| p.premise_type == PremiseType::Singular)
                .count();

            if universal_count >= 1 && singular_count >= 1 {
                // Verify the singular premise relates to the universal
                // by checking for shared terms
                let universal_premise = argument
                    .premises
                    .iter()
                    .find(|p| p.premise_type == PremiseType::Universal)?;

                let singular_premise = argument
                    .premises
                    .iter()
                    .find(|p| p.premise_type == PremiseType::Singular)?;

                // Extract predicate from universal (e.g., "humans" from "All humans are mortal")
                let univ_lower = universal_premise.statement.to_lowercase();
                if univ_lower.starts_with("all ") {
                    if let Some(are_idx) = univ_lower.find(" are ") {
                        let subject_term = Self::clean_term(&univ_lower[4..are_idx]);

                        // Check if singular premise predicates the same term
                        // e.g., "Socrates is human" should match "humans" (with stemming consideration)
                        let sing_lower = singular_premise.statement.to_lowercase();
                        let subject_stem = subject_term.trim_end_matches('s');

                        if sing_lower.contains(&subject_term) || sing_lower.contains(subject_stem) {
                            return Some(ArgumentForm::CategoricalSyllogism);
                        }
                    }
                }
            }
        }

        None
    }

    /// Check if the argument is valid
    fn check_validity(&self, argument: &Argument) -> (ValidityStatus, String) {
        // Check if we detected a known valid form
        if let Some(form) = self.detect_argument_form(argument) {
            if form.is_valid_form() {
                return (
                    ValidityStatus::Valid,
                    format!("Argument follows valid {} pattern", form.description()),
                );
            }
        }

        // Check for obvious invalidity patterns
        let fallacies = self.detect_formal_fallacies(argument);
        if !fallacies.is_empty() {
            let fallacy_names: Vec<_> = fallacies.iter().map(|f| f.fallacy.pattern()).collect();
            return (
                ValidityStatus::Invalid,
                format!(
                    "Argument contains formal fallacy: {}",
                    fallacy_names.join(", ")
                ),
            );
        }

        // Default to undetermined for complex arguments
        (
            ValidityStatus::Undetermined,
            "Argument structure too complex for automated validation. Manual review recommended."
                .to_string(),
        )
    }

    /// Detect formal fallacies only
    fn detect_formal_fallacies(&self, argument: &Argument) -> Vec<DetectedFallacy> {
        let mut fallacies = Vec::new();

        // Check for affirming the consequent
        if let Some(fallacy) = self.check_affirming_consequent(argument) {
            fallacies.push(fallacy);
        }

        // Check for denying the antecedent
        if let Some(fallacy) = self.check_denying_antecedent(argument) {
            fallacies.push(fallacy);
        }

        // Check for undistributed middle in syllogisms
        if let Some(fallacy) = self.check_undistributed_middle(argument) {
            fallacies.push(fallacy);
        }

        fallacies
    }

    /// Detect all fallacies (formal and informal)
    fn detect_fallacies(&self, argument: &Argument) -> Vec<DetectedFallacy> {
        let mut fallacies = self.detect_formal_fallacies(argument);

        // Check for circular reasoning
        if let Some(fallacy) = self.check_circular_reasoning(argument) {
            fallacies.push(fallacy);
        }

        // Check for false dichotomy
        if let Some(fallacy) = self.check_false_dichotomy(argument) {
            fallacies.push(fallacy);
        }

        // Check for non sequitur (basic)
        if let Some(fallacy) = self.check_non_sequitur(argument) {
            fallacies.push(fallacy);
        }

        fallacies
    }

    /// Check for affirming the consequent: P->Q, Q |- P
    fn check_affirming_consequent(&self, argument: &Argument) -> Option<DetectedFallacy> {
        // Find conditional premise
        let conditional = argument
            .premises
            .iter()
            .enumerate()
            .find(|(_, p)| p.premise_type == PremiseType::Conditional)?;

        let cond_lower = conditional.1.statement.to_lowercase();

        // Extract consequent (after "then") - clean punctuation
        let then_idx = cond_lower.find(" then ")?;
        let consequent = Self::clean_term(&cond_lower[then_idx + 6..]);

        // Check if another premise affirms the consequent
        let affirming_premise = argument.premises.iter().enumerate().find(|(i, p)| {
            *i != conditional.0 && p.premise_type != PremiseType::Conditional && {
                let p_clean = Self::clean_term(&p.statement.to_lowercase());
                p_clean.contains(&consequent) || consequent.contains(&p_clean)
            }
        });

        if affirming_premise.is_some() {
            // Check if conclusion affirms the antecedent
            let antecedent = Self::clean_term(&cond_lower[3..then_idx]);
            let conclusion_clean = Self::clean_term(&argument.conclusion.to_lowercase());
            if conclusion_clean.contains(&antecedent)
                || antecedent.contains(&conclusion_clean)
                || Self::terms_match(&conclusion_clean, &antecedent)
            {
                return Some(
                    DetectedFallacy::new(
                        Fallacy::AffirmingConsequent,
                        0.85,
                        "Argument affirms the consequent of a conditional to conclude the antecedent",
                    )
                    .with_premises(vec![conditional.0])
                    .with_suggestion("Consider other possible causes for the consequent being true"),
                );
            }
        }

        None
    }

    /// Check if two terms match (handles minor variations like tense)
    fn terms_match(a: &str, b: &str) -> bool {
        if a == b {
            return true;
        }

        // Handle past tense variations (e.g., "it rained" vs "it rains")
        let a_words: Vec<&str> = a.split_whitespace().collect();
        let b_words: Vec<&str> = b.split_whitespace().collect();

        if a_words.len() == b_words.len() {
            let mut matches = 0;
            for (aw, bw) in a_words.iter().zip(b_words.iter()) {
                if aw == bw {
                    matches += 1;
                } else {
                    // Check for verb tense variations
                    let aw_stem = aw.trim_end_matches("ed").trim_end_matches('s');
                    let bw_stem = bw.trim_end_matches("ed").trim_end_matches('s');
                    if aw_stem == bw_stem {
                        matches += 1;
                    }
                }
            }
            return matches == a_words.len();
        }

        false
    }

    /// Check for denying the antecedent: P->Q, ~P |- ~Q
    fn check_denying_antecedent(&self, argument: &Argument) -> Option<DetectedFallacy> {
        // Find conditional premise
        let conditional = argument
            .premises
            .iter()
            .enumerate()
            .find(|(_, p)| p.premise_type == PremiseType::Conditional)?;

        let cond_lower = conditional.1.statement.to_lowercase();
        let then_idx = cond_lower.find(" then ")?;
        let antecedent = Self::clean_term(&cond_lower[3..then_idx]);
        let consequent = Self::clean_term(&cond_lower[then_idx + 6..]);

        // Check if another premise denies the antecedent
        let denying_premise = argument.premises.iter().enumerate().find(|(i, p)| {
            *i != conditional.0
                && p.statement.to_lowercase().contains(&antecedent)
                && (p.statement.to_lowercase().contains("not ")
                    || p.statement.to_lowercase().starts_with("no "))
        });

        if denying_premise.is_some() {
            // Check if conclusion denies the consequent
            if argument.conclusion.to_lowercase().contains(&consequent)
                && (argument.conclusion.to_lowercase().contains("not ")
                    || argument.conclusion.to_lowercase().starts_with("no "))
            {
                return Some(
                    DetectedFallacy::new(
                        Fallacy::DenyingAntecedent,
                        0.85,
                        "Argument denies the antecedent to conclude the negation of the consequent",
                    )
                    .with_premises(vec![conditional.0])
                    .with_suggestion("The consequent might still be true for other reasons"),
                );
            }
        }

        None
    }

    /// Check for undistributed middle in syllogisms
    fn check_undistributed_middle(&self, argument: &Argument) -> Option<DetectedFallacy> {
        // Need at least 2 universal premises for a syllogism
        let universals: Vec<_> = argument
            .premises
            .iter()
            .enumerate()
            .filter(|(_, p)| p.premise_type == PremiseType::Universal)
            .collect();

        if universals.len() < 2 {
            return None;
        }

        // Extract terms from "All X are Y" patterns
        let mut terms: Vec<HashSet<String>> = Vec::new();
        for (_, premise) in &universals {
            let lower = premise.statement.to_lowercase();
            if lower.starts_with("all ") {
                if let Some(are_idx) = lower.find(" are ") {
                    let subject = Self::clean_term(&lower[4..are_idx]);
                    let predicate = Self::clean_term(&lower[are_idx + 5..]);
                    let mut term_set = HashSet::new();
                    term_set.insert(subject);
                    term_set.insert(predicate);
                    terms.push(term_set);
                }
            }
        }

        if terms.len() >= 2 {
            // Find middle term (appears in both premises)
            let intersection: HashSet<_> = terms[0].intersection(&terms[1]).cloned().collect();

            if intersection.is_empty() {
                // No shared term - possible four-term fallacy or undistributed middle
                return Some(
                    DetectedFallacy::new(
                        Fallacy::UndistributedMiddle,
                        0.75,
                        "The middle term may not be properly distributed across premises",
                    )
                    .with_premises(vec![universals[0].0, universals[1].0])
                    .with_suggestion(
                        "Ensure the middle term is distributed in at least one premise",
                    ),
                );
            }
        }

        None
    }

    /// Check for circular reasoning
    fn check_circular_reasoning(&self, argument: &Argument) -> Option<DetectedFallacy> {
        let conclusion_lower = argument.conclusion.to_lowercase();
        let conclusion_words: HashSet<_> = conclusion_lower
            .split_whitespace()
            .filter(|w| w.len() > 3)
            .collect();

        // Need at least 2 significant words in conclusion to detect circular reasoning
        // This prevents false positives with very short conclusions
        if conclusion_words.len() < 2 {
            return None;
        }

        for (idx, premise) in argument.premises.iter().enumerate() {
            let premise_lower = premise.statement.to_lowercase();
            let premise_words: HashSet<_> = premise_lower
                .split_whitespace()
                .filter(|w| w.len() > 3)
                .collect();

            // For circular reasoning, check if the conclusion is essentially
            // restating something from the premise.
            let overlap = conclusion_words.intersection(&premise_words).count();
            let conclusion_len = conclusion_words.len();

            // Circular reasoning detection:
            // - If conclusion words are mostly found in premise (>= 80% overlap with conclusion)
            // - OR if we have at least 2 overlapping significant words with high ratio
            let conclusion_overlap_ratio = overlap as f64 / conclusion_len as f64;

            // High overlap with conclusion means the conclusion restates the premise
            if overlap >= 2 && conclusion_overlap_ratio >= 0.8 {
                return Some(
                    DetectedFallacy::new(
                        Fallacy::CircularReasoning,
                        0.7,
                        "Premise and conclusion appear to state essentially the same thing",
                    )
                    .with_premises(vec![idx])
                    .with_suggestion(
                        "Provide independent evidence that doesn't restate the conclusion",
                    ),
                );
            }
        }

        None
    }

    /// Check for false dichotomy
    fn check_false_dichotomy(&self, argument: &Argument) -> Option<DetectedFallacy> {
        // Look for "either...or" patterns without "or" alternatives
        for (idx, premise) in argument.premises.iter().enumerate() {
            let lower = premise.statement.to_lowercase();

            if (lower.contains("either ") && lower.contains(" or ")) || lower.contains(" only ") {
                // Check if it presents just two options
                let or_count = lower.matches(" or ").count();
                if or_count == 1 {
                    return Some(
                        DetectedFallacy::new(
                            Fallacy::FalseDichotomy,
                            0.6,
                            "Argument presents only two options when more may exist",
                        )
                        .with_premises(vec![idx])
                        .with_suggestion("Consider whether additional alternatives exist"),
                    );
                }
            }
        }

        None
    }

    /// Check for basic non sequitur
    fn check_non_sequitur(&self, argument: &Argument) -> Option<DetectedFallacy> {
        // Very basic check: are there any shared significant terms between premises and conclusion?
        let conclusion_words: HashSet<_> = argument
            .conclusion
            .to_lowercase()
            .split_whitespace()
            .filter(|w| w.len() > 4)
            .map(|s| s.to_string())
            .collect();

        let mut any_overlap = false;
        for premise in &argument.premises {
            let premise_words: HashSet<_> = premise
                .statement
                .to_lowercase()
                .split_whitespace()
                .filter(|w| w.len() > 4)
                .map(|s| s.to_string())
                .collect();

            if !conclusion_words.is_disjoint(&premise_words) {
                any_overlap = true;
                break;
            }
        }

        if !any_overlap && !conclusion_words.is_empty() {
            return Some(
                DetectedFallacy::new(
                    Fallacy::NonSequitur,
                    0.5,
                    "Conclusion appears disconnected from the premises",
                )
                .with_suggestion(
                    "Establish a clear logical connection between premises and conclusion",
                ),
            );
        }

        None
    }

    /// Detect contradictions in the argument
    fn detect_contradictions(&self, argument: &Argument) -> Vec<Contradiction> {
        let mut contradictions = Vec::new();

        // Check each pair of premises
        for (i, p1) in argument.premises.iter().enumerate() {
            for (j, p2) in argument.premises.iter().enumerate().skip(i + 1) {
                if let Some(contradiction) = self.check_contradiction(&p1.statement, &p2.statement)
                {
                    contradictions.push(Contradiction {
                        statement_a: format!("Premise {}", i + 1),
                        statement_b: format!("Premise {}", j + 1),
                        contradiction_type: contradiction.0,
                        explanation: contradiction.1,
                    });
                }
            }
        }

        // Check premises against conclusion
        for (i, premise) in argument.premises.iter().enumerate() {
            if let Some(contradiction) =
                self.check_contradiction(&premise.statement, &argument.conclusion)
            {
                contradictions.push(Contradiction {
                    statement_a: format!("Premise {}", i + 1),
                    statement_b: "Conclusion".to_string(),
                    contradiction_type: contradiction.0,
                    explanation: contradiction.1,
                });
            }
        }

        contradictions
    }

    /// Check if two statements contradict
    fn check_contradiction(&self, a: &str, b: &str) -> Option<(ContradictionType, String)> {
        let a_lower = a.to_lowercase();
        let b_lower = b.to_lowercase();

        // Check for direct negation patterns
        let negation_patterns = [
            ("is true", "is false"),
            ("exists", "does not exist"),
            ("is valid", "is invalid"),
            ("should", "should not"),
            ("must", "must not"),
            ("always", "never"),
            ("all", "none"),
            ("is ", "is not "),
            ("can ", "cannot "),
            ("will ", "will not "),
        ];

        for (pos, neg) in &negation_patterns {
            if (a_lower.contains(pos) && b_lower.contains(neg))
                || (a_lower.contains(neg) && b_lower.contains(pos))
            {
                // Check for subject overlap (with relaxed filtering for short subjects)
                if self.have_subject_overlap(&a_lower, &b_lower) {
                    return Some((
                        ContradictionType::DirectNegation,
                        format!(
                            "Direct contradiction detected: one states '{}' while other states '{}'",
                            pos, neg
                        ),
                    ));
                }
            }
        }

        None
    }

    /// Check if two statements share a common subject
    fn have_subject_overlap(&self, a: &str, b: &str) -> bool {
        let stopwords: HashSet<&str> = [
            "the", "a", "an", "is", "are", "was", "were", "be", "been", "being", "have", "has",
            "had", "do", "does", "did", "will", "would", "could", "should", "may", "might", "must",
            "shall", "can", "need", "dare", "ought", "used", "to", "of", "in", "for", "on", "with",
            "at", "by", "from", "as", "into", "through", "during", "before", "after", "above",
            "below", "between", "under", "again", "further", "then", "once", "that", "this",
            "these", "those", "not", "no", "nor", "and", "but", "or", "if", "while", "because",
            "until", "although", "since", "when", "where", "why", "how", "all", "each", "every",
            "both", "few", "more", "most", "other", "some", "such", "only", "own", "same", "so",
            "than", "too", "very", "just", "true", "false",
        ]
        .iter()
        .cloned()
        .collect();

        // Use minimum length of 1 to catch single-letter subjects like "X"
        let words_a: HashSet<&str> = a
            .split_whitespace()
            .filter(|w| !stopwords.contains(w) && !w.is_empty())
            .collect();

        let words_b: HashSet<&str> = b
            .split_whitespace()
            .filter(|w| !stopwords.contains(w) && !w.is_empty())
            .collect();

        if words_a.is_empty() || words_b.is_empty() {
            // If both have the same structure after removing stopwords,
            // check if they're talking about the same subject
            // For "X is true" vs "X is false", both reduce to just "x"
            return true;
        }

        let overlap = words_a.intersection(&words_b).count();

        // If there's any overlap, consider it a match
        overlap > 0
    }

    /// Check soundness (valid + true premises)
    fn check_soundness(
        &self,
        argument: &Argument,
        validity: ValidityStatus,
    ) -> (SoundnessStatus, String) {
        if validity != ValidityStatus::Valid {
            return (
                SoundnessStatus::Unsound,
                "Argument is invalid, therefore unsound".to_string(),
            );
        }

        // Calculate average premise confidence
        let avg_confidence: f64 = argument.premises.iter().map(|p| p.confidence).sum::<f64>()
            / argument.premises.len() as f64;

        if avg_confidence >= self.analysis_config.confidence_threshold {
            (
                SoundnessStatus::Sound,
                format!(
                    "Argument is valid and premises have high confidence ({:.0}%)",
                    avg_confidence * 100.0
                ),
            )
        } else if avg_confidence >= 0.5 {
            (
                SoundnessStatus::Undetermined,
                format!(
                    "Argument is valid but premise truth is uncertain ({:.0}% confidence)",
                    avg_confidence * 100.0
                ),
            )
        } else {
            (
                SoundnessStatus::Unsound,
                format!(
                    "Argument is valid but premises have low confidence ({:.0}%)",
                    avg_confidence * 100.0
                ),
            )
        }
    }

    /// Calculate overall confidence in the analysis
    fn calculate_confidence(&self, result: &LaserLogicResult) -> f64 {
        let mut confidence = 0.7; // Base confidence

        // Boost for detected form
        if result.argument_form.is_some() {
            confidence += 0.1;
        }

        // Boost for determined validity
        if result.validity != ValidityStatus::Undetermined {
            confidence += 0.1;
        }

        // Penalty for detected fallacies
        let fallacy_penalty = result.fallacies.len() as f64 * 0.05;
        confidence -= fallacy_penalty.min(0.2);

        // Penalty for contradictions
        if !result.contradictions.is_empty() {
            confidence -= 0.15;
        }

        confidence.clamp(0.0, 1.0)
    }

    /// Generate suggestions for improving the argument
    fn generate_suggestions(&self, result: &LaserLogicResult) -> Vec<String> {
        let mut suggestions = Vec::new();

        // Suggestions based on validity
        if result.validity == ValidityStatus::Invalid {
            suggestions.push(
                "Restructure the argument to ensure the conclusion follows logically from the premises."
                    .to_string(),
            );
        }

        // Suggestions based on fallacies
        for fallacy in &result.fallacies {
            if !fallacy.suggestion.is_empty() {
                suggestions.push(fallacy.suggestion.clone());
            }
        }

        // Suggestions based on contradictions
        if !result.contradictions.is_empty() {
            suggestions.push(
                "Resolve contradictions by revising conflicting premises or clarifying terms."
                    .to_string(),
            );
        }

        // Suggestions based on soundness
        if result.soundness == SoundnessStatus::Undetermined {
            suggestions
                .push("Provide additional evidence to support premise truth claims.".to_string());
        }

        // Argument form suggestions
        if result.argument_form.is_none() {
            suggestions.push(
                "Consider restructuring into a standard argument form (modus ponens, syllogism, etc.) for clarity."
                    .to_string(),
            );
        }

        // Deduplicate
        suggestions.sort();
        suggestions.dedup();

        suggestions
    }
}

impl ThinkToolModule for LaserLogic {
    fn config(&self) -> &ThinkToolModuleConfig {
        &self.config
    }

    fn execute(&self, context: &ThinkToolContext) -> Result<ThinkToolOutput> {
        // Parse the query as an argument
        // Expected format: "Premise 1. Premise 2. Therefore, Conclusion."
        // Or: premises separated by semicolons, conclusion after "therefore" or "hence"

        let query = &context.query;

        // Try to parse premises and conclusion from the query
        let (premises, conclusion) = self.parse_argument_from_query(query)?;

        // Analyze the argument
        let result = self.analyze_argument(&premises, conclusion)?;

        // Convert to ThinkToolOutput
        Ok(ThinkToolOutput {
            module: self.config.name.clone(),
            confidence: result.confidence,
            output: serde_json::json!({
                "validity": format!("{:?}", result.validity),
                "validity_explanation": result.validity_explanation,
                "soundness": format!("{:?}", result.soundness),
                "soundness_explanation": result.soundness_explanation,
                "argument_form": result.argument_form.map(|f| f.description()),
                "fallacies": result.fallacies.iter().map(|f| {
                    serde_json::json!({
                        "type": format!("{:?}", f.fallacy),
                        "description": f.fallacy.description(),
                        "pattern": f.fallacy.pattern(),
                        "confidence": f.confidence,
                        "evidence": f.evidence,
                        "suggestion": f.suggestion
                    })
                }).collect::<Vec<_>>(),
                "contradictions": result.contradictions.iter().map(|c| {
                    serde_json::json!({
                        "between": [c.statement_a, c.statement_b],
                        "type": format!("{:?}", c.contradiction_type),
                        "explanation": c.explanation
                    })
                }).collect::<Vec<_>>(),
                "verdict": result.verdict(),
                "suggestions": result.suggestions,
                "reasoning_steps": result.reasoning_steps
            }),
        })
    }
}

impl LaserLogic {
    /// Parse an argument from a natural language query
    fn parse_argument_from_query<'a>(&self, query: &'a str) -> Result<(Vec<&'a str>, &'a str)> {
        let query = query.trim();

        // Look for conclusion markers
        let conclusion_markers = [
            "therefore,",
            "therefore",
            "hence,",
            "hence",
            "thus,",
            "thus",
            "so,",
            "consequently,",
            "consequently",
            "it follows that",
            "we can conclude",
            "which means",
        ];

        for marker in &conclusion_markers {
            if let Some(idx) = query.to_lowercase().find(marker) {
                let premises_part = &query[..idx];
                let conclusion_start = idx + marker.len();
                let conclusion = query[conclusion_start..]
                    .trim()
                    .trim_start_matches(',')
                    .trim();

                // Parse premises (split by period, semicolon, or "and")
                let premises: Vec<&str> = premises_part
                    .split(['.', ';'])
                    .map(|s| s.trim())
                    .filter(|s| !s.is_empty())
                    .collect();

                if !premises.is_empty() && !conclusion.is_empty() {
                    return Ok((premises, conclusion));
                }
            }
        }

        // Fallback: try splitting by sentences
        let sentences: Vec<&str> = query
            .split('.')
            .map(|s| s.trim())
            .filter(|s| !s.is_empty())
            .collect();

        if sentences.len() >= 2 {
            let premises = &sentences[..sentences.len() - 1];
            let conclusion = sentences.last().unwrap();
            return Ok((premises.to_vec(), conclusion));
        }

        Err(Error::validation(
            "Could not parse argument structure. Expected format: 'Premise 1. Premise 2. Therefore, Conclusion.' or similar.",
        ))
    }
}

// =============================================================================
// Tests
// =============================================================================

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_config_default() {
        let config = LaserLogicConfig::default();
        assert!(config.detect_fallacies);
        assert!(config.check_validity);
        assert!(config.check_soundness);
    }

    #[test]
    fn test_config_presets() {
        let quick = LaserLogicConfig::quick();
        assert!(!quick.check_soundness);
        assert_eq!(quick.max_premise_depth, 5);

        let deep = LaserLogicConfig::deep();
        assert!(deep.check_soundness);
        assert!(deep.verbose_output);

        let paranoid = LaserLogicConfig::paranoid();
        assert_eq!(paranoid.confidence_threshold, 0.9);
    }

    #[test]
    fn test_premise_type_inference() {
        assert_eq!(
            Premise::new("All humans are mortal").premise_type,
            PremiseType::Universal
        );
        assert_eq!(
            Premise::new("Some birds can fly").premise_type,
            PremiseType::Particular
        );
        assert_eq!(
            Premise::new("If it rains, the ground is wet").premise_type,
            PremiseType::Conditional
        );
        assert_eq!(
            Premise::new("Either we go or we stay").premise_type,
            PremiseType::Disjunctive
        );
        assert_eq!(
            Premise::new("Socrates is human").premise_type,
            PremiseType::Singular
        );
    }

    #[test]
    fn test_fallacy_descriptions() {
        let fallacy = Fallacy::AffirmingConsequent;
        assert!(fallacy.description().contains("Inferring"));
        assert!(fallacy.pattern().contains("INVALID"));
        assert!(fallacy.is_formal());
        assert_eq!(fallacy.severity(), 5);
    }

    #[test]
    fn test_valid_modus_ponens() {
        let laser = LaserLogic::new();
        let result = laser
            .analyze_argument(
                &["If it rains, then the ground is wet", "It rains"],
                "The ground is wet",
            )
            .unwrap();

        // Should detect modus ponens form
        assert!(result.argument_form.is_some());
        assert!(!result.has_fallacies());
    }

    #[test]
    fn test_affirming_consequent_detection() {
        let laser = LaserLogic::new();
        let result = laser
            .analyze_argument(
                &["If it rains, then the ground is wet", "The ground is wet"],
                "It rained",
            )
            .unwrap();

        // Should detect affirming the consequent
        assert!(result.has_fallacies());
        assert!(result
            .fallacies
            .iter()
            .any(|f| f.fallacy == Fallacy::AffirmingConsequent));
    }

    #[test]
    fn test_categorical_syllogism() {
        let laser = LaserLogic::new();
        let result = laser
            .analyze_argument(
                &["All humans are mortal", "All Greeks are humans"],
                "All Greeks are mortal",
            )
            .unwrap();

        assert_eq!(
            result.argument_form,
            Some(ArgumentForm::CategoricalSyllogism)
        );
    }

    #[test]
    fn test_circular_reasoning_detection() {
        let laser = LaserLogic::new();
        let result = laser
            .analyze_argument(
                &["The Bible is true because it is the word of God"],
                "The Bible is the word of God",
            )
            .unwrap();

        assert!(result
            .fallacies
            .iter()
            .any(|f| f.fallacy == Fallacy::CircularReasoning));
    }

    #[test]
    fn test_contradiction_detection() {
        let laser = LaserLogic::with_config(LaserLogicConfig::deep());
        let result = laser
            .analyze_argument(&["X is true", "X is false"], "Something follows")
            .unwrap();

        assert!(!result.contradictions.is_empty());
    }

    #[test]
    fn test_thinkmodule_trait() {
        let laser = LaserLogic::new();
        let config = laser.config();
        assert_eq!(config.name, "LaserLogic");
        assert_eq!(config.version, "3.0.0");
    }

    #[test]
    fn test_execute_with_context() {
        let laser = LaserLogic::new();
        let context = ThinkToolContext {
            query: "All humans are mortal. Socrates is human. Therefore, Socrates is mortal."
                .to_string(),
            previous_steps: vec![],
        };

        let output = laser.execute(&context).unwrap();
        assert_eq!(output.module, "LaserLogic");
        assert!(output.confidence > 0.0);
    }

    #[test]
    fn test_verdict_generation() {
        let mut result = LaserLogicResult::new(Argument::new(vec!["premise"], "conclusion"));
        result.validity = ValidityStatus::Valid;
        result.soundness = SoundnessStatus::Sound;
        assert!(result.verdict().contains("SOUND"));

        result.validity = ValidityStatus::Invalid;
        assert!(result.verdict().contains("INVALID"));
    }

    #[test]
    fn test_argument_form_validity() {
        assert!(ArgumentForm::ModusPonens.is_valid_form());
        assert!(ArgumentForm::ModusTollens.is_valid_form());
        assert!(!ArgumentForm::Unknown.is_valid_form());
    }

    #[test]
    fn test_empty_premises_error() {
        let laser = LaserLogic::new();
        let result = laser.analyze_argument(&[], "Some conclusion");
        assert!(result.is_err());
    }

    #[test]
    fn test_too_many_premises_error() {
        let laser = LaserLogic::with_config(LaserLogicConfig {
            max_premise_depth: 2,
            ..Default::default()
        });
        let result = laser.analyze_argument(&["P1", "P2", "P3"], "Conclusion");
        assert!(result.is_err());
    }
}