reasonkit/thinktool/
deep_logic.rs

1//! # Deep Logic Module - Neuro-Symbolic Reasoning Framework
2//!
3//! Implements a hybrid neuro-symbolic reasoning system that combines:
4//! - Neural (LLM) pattern recognition with symbolic rule validation
5//! - Logical constraint enforcement
6//! - Inference rules and deduction
7//! - Contradiction detection
8//! - Formal verification hooks
9//!
10//! This bridges the gap between LLM reasoning and formal logic systems.
11//!
12//! ## Usage
13//!
14//! ```rust,ignore
15//! use reasonkit::thinktool::deep_logic::{DeepLogicValidator, LogicalConstraint, InferenceRule};
16//!
17//! let mut validator = DeepLogicValidator::new();
18//!
19//! // Add constraints
20//! validator.add_constraint(LogicalConstraint::equality("age", "18", "Age must be 18"));
21//!
22//! // Add inference rules
23//! validator.add_rule(InferenceRule::new("adult_rule")
24//!     .with_premise(LogicalConstraint::greater("age", "17"))
25//!     .with_conclusion("is_adult"));
26//!
27//! // Validate data
28//! let result = validator.validate(&data).await?;
29//! ```
30
31use serde::{Deserialize, Serialize};
32use std::collections::HashMap;
33use std::fmt;
34
35// =============================================================================
36// Logical Primitives
37// =============================================================================
38
39/// Logical operators for rule composition
40#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
41pub enum LogicalOperator {
42    /// Logical AND
43    And,
44    /// Logical OR
45    Or,
46    /// Logical NOT
47    Not,
48    /// Implication (if-then)
49    Implies,
50    /// If and only if (biconditional)
51    Iff,
52    /// Exclusive OR
53    Xor,
54}
55
56/// Types of logical constraints
57#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
58pub enum ConstraintType {
59    /// A == B
60    Equality,
61    /// A != B
62    Inequality,
63    /// A > B
64    Greater,
65    /// A < B
66    Less,
67    /// A in B (contains)
68    Contains,
69    /// A matches pattern B (regex)
70    Matches,
71    /// type(A) == B
72    TypeCheck,
73    /// A in [min, max]
74    Range,
75    /// Custom predicate
76    Custom,
77}
78
79/// Results of constraint validation
80#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
81pub enum ValidationResult {
82    /// Constraint is satisfied
83    Valid,
84    /// Constraint is violated
85    Invalid,
86    /// Cannot determine
87    Unknown,
88    /// Partially satisfied
89    Partial,
90}
91
92// =============================================================================
93// Constraint and Rule Models
94// =============================================================================
95
96/// A single logical constraint
97#[derive(Debug, Clone, Serialize, Deserialize)]
98pub struct LogicalConstraint {
99    /// Unique identifier
100    pub constraint_id: String,
101    /// Type of constraint
102    pub constraint_type: ConstraintType,
103    /// Human-readable description
104    pub description: String,
105    /// Left operand (key or value)
106    pub left_operand: String,
107    /// Right operand (optional, for unary constraints)
108    pub right_operand: Option<String>,
109    /// Operator value (for type/pattern checks)
110    pub operator_value: Option<String>,
111    /// Is this constraint required?
112    pub is_required: bool,
113    /// Error message if violated
114    pub error_message: String,
115}
116
117impl LogicalConstraint {
118    /// Create a new constraint
119    pub fn new(
120        constraint_id: String,
121        constraint_type: ConstraintType,
122        left_operand: String,
123    ) -> Self {
124        Self {
125            constraint_id,
126            constraint_type,
127            description: String::new(),
128            left_operand,
129            right_operand: None,
130            operator_value: None,
131            is_required: true,
132            error_message: String::new(),
133        }
134    }
135
136    /// Create an equality constraint
137    pub fn equality(left: &str, right: &str, description: &str) -> Self {
138        Self {
139            constraint_id: format!("eq_{}_{}", left, right),
140            constraint_type: ConstraintType::Equality,
141            description: description.to_string(),
142            left_operand: left.to_string(),
143            right_operand: Some(right.to_string()),
144            operator_value: None,
145            is_required: true,
146            error_message: format!("{} must equal {}", left, right),
147        }
148    }
149
150    /// Create a greater-than constraint
151    pub fn greater(left: &str, right: &str, description: &str) -> Self {
152        Self {
153            constraint_id: format!("gt_{}_{}", left, right),
154            constraint_type: ConstraintType::Greater,
155            description: description.to_string(),
156            left_operand: left.to_string(),
157            right_operand: Some(right.to_string()),
158            operator_value: None,
159            is_required: true,
160            error_message: format!("{} must be greater than {}", left, right),
161        }
162    }
163
164    /// Create a less-than constraint
165    pub fn less(left: &str, right: &str, description: &str) -> Self {
166        Self {
167            constraint_id: format!("lt_{}_{}", left, right),
168            constraint_type: ConstraintType::Less,
169            description: description.to_string(),
170            left_operand: left.to_string(),
171            right_operand: Some(right.to_string()),
172            operator_value: None,
173            is_required: true,
174            error_message: format!("{} must be less than {}", left, right),
175        }
176    }
177
178    /// Create a type check constraint
179    pub fn type_check(operand: &str, expected_type: &str, description: &str) -> Self {
180        Self {
181            constraint_id: format!("type_{}_{}", operand, expected_type),
182            constraint_type: ConstraintType::TypeCheck,
183            description: description.to_string(),
184            left_operand: operand.to_string(),
185            right_operand: None,
186            operator_value: Some(expected_type.to_string()),
187            is_required: true,
188            error_message: format!("{} must be of type {}", operand, expected_type),
189        }
190    }
191
192    /// Set description
193    pub fn with_description(mut self, description: &str) -> Self {
194        self.description = description.to_string();
195        self
196    }
197
198    /// Set error message
199    pub fn with_error_message(mut self, message: &str) -> Self {
200        self.error_message = message.to_string();
201        self
202    }
203
204    /// Set required flag
205    pub fn with_required(mut self, required: bool) -> Self {
206        self.is_required = required;
207        self
208    }
209}
210
211impl fmt::Display for LogicalConstraint {
212    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
213        match self.constraint_type {
214            ConstraintType::Equality => {
215                write!(
216                    f,
217                    "{} == {}",
218                    self.left_operand,
219                    self.right_operand.as_deref().unwrap_or("?")
220                )
221            }
222            ConstraintType::Inequality => {
223                write!(
224                    f,
225                    "{} != {}",
226                    self.left_operand,
227                    self.right_operand.as_deref().unwrap_or("?")
228                )
229            }
230            ConstraintType::Greater => {
231                write!(
232                    f,
233                    "{} > {}",
234                    self.left_operand,
235                    self.right_operand.as_deref().unwrap_or("?")
236                )
237            }
238            ConstraintType::Less => {
239                write!(
240                    f,
241                    "{} < {}",
242                    self.left_operand,
243                    self.right_operand.as_deref().unwrap_or("?")
244                )
245            }
246            ConstraintType::Contains => {
247                write!(
248                    f,
249                    "{} in {}",
250                    self.left_operand,
251                    self.right_operand.as_deref().unwrap_or("?")
252                )
253            }
254            ConstraintType::Matches => {
255                write!(
256                    f,
257                    "{} matches {}",
258                    self.left_operand,
259                    self.operator_value.as_deref().unwrap_or("?")
260                )
261            }
262            ConstraintType::TypeCheck => {
263                write!(
264                    f,
265                    "type({}) == {}",
266                    self.left_operand,
267                    self.operator_value.as_deref().unwrap_or("?")
268                )
269            }
270            _ => {
271                if !self.description.is_empty() {
272                    write!(f, "{}", self.description)
273                } else {
274                    write!(f, "{}", self.constraint_id)
275                }
276            }
277        }
278    }
279}
280
281/// A logical inference rule (if-then)
282#[derive(Debug, Clone, Serialize, Deserialize)]
283pub struct InferenceRule {
284    /// Unique identifier
285    pub rule_id: String,
286    /// Human-readable name
287    pub name: String,
288    /// Description
289    pub description: String,
290    /// Premises (conditions that must be true)
291    pub premises: Vec<LogicalConstraint>,
292    /// Conclusions (what becomes true if premises hold)
293    pub conclusions: Vec<String>,
294    /// Logical operator for combining premises
295    pub combine_with: LogicalOperator,
296    /// Priority (higher = earlier evaluation)
297    pub priority: i32,
298    /// Is this a default rule?
299    pub is_default_rule: bool,
300}
301
302impl InferenceRule {
303    /// Create a new inference rule
304    pub fn new(rule_id: &str) -> Self {
305        Self {
306            rule_id: rule_id.to_string(),
307            name: rule_id.to_string(),
308            description: String::new(),
309            premises: Vec::new(),
310            conclusions: Vec::new(),
311            combine_with: LogicalOperator::And,
312            priority: 0,
313            is_default_rule: false,
314        }
315    }
316
317    /// Set name
318    pub fn with_name(mut self, name: &str) -> Self {
319        self.name = name.to_string();
320        self
321    }
322
323    /// Set description
324    pub fn with_description(mut self, description: &str) -> Self {
325        self.description = description.to_string();
326        self
327    }
328
329    /// Add a premise constraint
330    pub fn with_premise(mut self, constraint: LogicalConstraint) -> Self {
331        self.premises.push(constraint);
332        self
333    }
334
335    /// Add a conclusion
336    pub fn with_conclusion(mut self, conclusion: &str) -> Self {
337        self.conclusions.push(conclusion.to_string());
338        self
339    }
340
341    /// Set logical operator for combining premises
342    pub fn with_operator(mut self, op: LogicalOperator) -> Self {
343        self.combine_with = op;
344        self
345    }
346
347    /// Set priority
348    pub fn with_priority(mut self, priority: i32) -> Self {
349        self.priority = priority;
350        self
351    }
352
353    /// Mark as default rule
354    pub fn as_default(mut self) -> Self {
355        self.is_default_rule = true;
356        self
357    }
358}
359
360/// A logical fact in the knowledge base
361#[derive(Debug, Clone, Serialize, Deserialize)]
362pub struct LogicalFact {
363    /// Unique identifier
364    pub fact_id: String,
365    /// Statement
366    pub statement: String,
367    /// Confidence (0.0 - 1.0)
368    pub confidence: f64,
369    /// Derived from (rule or constraint IDs)
370    pub derived_from: Vec<String>,
371    /// Source (asserted, derived, external)
372    pub source: String,
373    /// Is persistent?
374    pub is_persistent: bool,
375}
376
377impl LogicalFact {
378    /// Create a new fact
379    pub fn new(fact_id: &str, statement: &str, confidence: f64) -> Self {
380        Self {
381            fact_id: fact_id.to_string(),
382            statement: statement.to_string(),
383            confidence,
384            derived_from: Vec::new(),
385            source: "asserted".to_string(),
386            is_persistent: true,
387        }
388    }
389
390    /// Create a derived fact
391    pub fn derived(fact_id: &str, statement: &str, from: &str) -> Self {
392        Self {
393            fact_id: fact_id.to_string(),
394            statement: statement.to_string(),
395            confidence: 1.0,
396            derived_from: vec![from.to_string()],
397            source: "derived".to_string(),
398            is_persistent: true,
399        }
400    }
401}
402
403/// Information about a detected contradiction
404#[derive(Debug, Clone, Serialize, Deserialize)]
405pub struct ContradictionInfo {
406    /// Unique identifier
407    pub contradiction_id: String,
408    /// Description
409    pub description: String,
410    /// Conflicting fact A
411    pub fact_a: String,
412    /// Conflicting fact B
413    pub fact_b: String,
414    /// Source rule (if applicable)
415    pub source_rule: Option<String>,
416    /// Source constraint (if applicable)
417    pub source_constraint: Option<String>,
418    /// Is resolved?
419    pub resolved: bool,
420    /// Resolution method
421    pub resolution_method: Option<String>,
422    /// Resolution fact
423    pub resolution_fact: Option<String>,
424}
425
426// =============================================================================
427// Validation Results
428// =============================================================================
429
430/// Result of validating a single constraint
431#[derive(Debug, Clone, Serialize, Deserialize)]
432pub struct ConstraintValidationResult {
433    /// The constraint that was validated
434    pub constraint: LogicalConstraint,
435    /// Validation result
436    pub result: ValidationResult,
437    /// Actual value found
438    pub actual_value: Option<serde_json::Value>,
439    /// Expected value
440    pub expected_value: Option<serde_json::Value>,
441    /// Error message
442    pub error_message: String,
443}
444
445/// Result of validating an inference rule
446#[derive(Debug, Clone, Serialize, Deserialize)]
447pub struct RuleValidationResult {
448    /// The rule that was validated
449    pub rule: InferenceRule,
450    /// Were all premises satisfied?
451    pub premises_satisfied: bool,
452    /// Results for each premise
453    pub premise_results: Vec<ConstraintValidationResult>,
454    /// Conclusions that were derived
455    pub conclusions_derived: Vec<String>,
456}
457
458/// Complete deep logic validation result
459#[derive(Debug, Clone, Serialize, Deserialize)]
460pub struct DeepLogicValidation {
461    /// Overall validity
462    pub is_valid: bool,
463    /// Confidence (0.0 - 1.0)
464    pub confidence: f64,
465    /// Constraint results
466    pub constraint_results: Vec<ConstraintValidationResult>,
467    /// Number of constraints satisfied
468    pub constraints_satisfied: usize,
469    /// Number of constraints violated
470    pub constraints_violated: usize,
471    /// Rule results
472    pub rule_results: Vec<RuleValidationResult>,
473    /// Number of rules applied
474    pub rules_applied: usize,
475    /// Facts derived
476    pub facts_derived: Vec<LogicalFact>,
477    /// Contradictions detected
478    pub contradictions: Vec<ContradictionInfo>,
479    /// Has contradictions?
480    pub has_contradictions: bool,
481    /// Errors
482    pub errors: Vec<String>,
483    /// Warnings
484    pub warnings: Vec<String>,
485    /// Recommendations
486    pub recommendations: Vec<String>,
487}
488
489impl DeepLogicValidation {
490    /// Create a new validation result
491    pub fn new(is_valid: bool) -> Self {
492        Self {
493            is_valid,
494            confidence: 0.0,
495            constraint_results: Vec::new(),
496            constraints_satisfied: 0,
497            constraints_violated: 0,
498            rule_results: Vec::new(),
499            rules_applied: 0,
500            facts_derived: Vec::new(),
501            contradictions: Vec::new(),
502            has_contradictions: false,
503            errors: Vec::new(),
504            warnings: Vec::new(),
505            recommendations: Vec::new(),
506        }
507    }
508}
509
510// =============================================================================
511// Constraint Evaluator
512// =============================================================================
513
514/// Evaluates logical constraints against data
515/// Type alias for custom predicate functions
516type CustomPredicate =
517    Box<dyn Fn(&serde_json::Value, Option<&serde_json::Value>) -> bool + Send + Sync>;
518
519pub struct ConstraintEvaluator {
520    /// Custom predicate functions
521    custom_predicates: HashMap<String, CustomPredicate>,
522}
523
524impl ConstraintEvaluator {
525    /// Create a new constraint evaluator
526    pub fn new() -> Self {
527        Self {
528            custom_predicates: HashMap::new(),
529        }
530    }
531
532    /// Register a custom predicate function
533    pub fn register_predicate<F>(&mut self, name: &str, predicate: F)
534    where
535        F: Fn(&serde_json::Value, Option<&serde_json::Value>) -> bool + Send + Sync + 'static,
536    {
537        self.custom_predicates
538            .insert(name.to_string(), Box::new(predicate));
539    }
540
541    /// Evaluate a constraint against data
542    pub fn evaluate(
543        &self,
544        constraint: &LogicalConstraint,
545        data: &serde_json::Value,
546    ) -> ConstraintValidationResult {
547        match self.try_evaluate(constraint, data) {
548            Ok((result, actual, expected)) => ConstraintValidationResult {
549                constraint: constraint.clone(),
550                result,
551                actual_value: actual,
552                expected_value: expected,
553                error_message: if result == ValidationResult::Valid {
554                    String::new()
555                } else {
556                    constraint.error_message.clone()
557                },
558            },
559            Err(e) => ConstraintValidationResult {
560                constraint: constraint.clone(),
561                result: ValidationResult::Unknown,
562                actual_value: None,
563                expected_value: None,
564                error_message: e,
565            },
566        }
567    }
568
569    fn try_evaluate(
570        &self,
571        constraint: &LogicalConstraint,
572        data: &serde_json::Value,
573    ) -> Result<
574        (
575            ValidationResult,
576            Option<serde_json::Value>,
577            Option<serde_json::Value>,
578        ),
579        String,
580    > {
581        let left_value = self.resolve_operand(&constraint.left_operand, data)?;
582        let right_value = constraint
583            .right_operand
584            .as_ref()
585            .map(|op| self.resolve_operand(op, data))
586            .transpose()?;
587
588        let result = self.evaluate_constraint_type(
589            constraint.constraint_type,
590            &left_value,
591            right_value.as_ref(),
592            constraint.operator_value.as_deref(),
593        )?;
594
595        Ok((
596            if result {
597                ValidationResult::Valid
598            } else {
599                ValidationResult::Invalid
600            },
601            Some(left_value),
602            right_value,
603        ))
604    }
605
606    fn resolve_operand(
607        &self,
608        operand: &str,
609        data: &serde_json::Value,
610    ) -> Result<serde_json::Value, String> {
611        if operand.starts_with('$') {
612            // Variable reference: $field.subfield
613            let path = operand.strip_prefix('$').unwrap_or(operand).split('.');
614            let mut value = data;
615            for key in path {
616                value = value
617                    .get(key)
618                    .ok_or_else(|| format!("Cannot resolve {}", operand))?;
619            }
620            Ok(value.clone())
621        } else if operand.starts_with('"') && operand.ends_with('"') {
622            // Literal string
623            Ok(serde_json::Value::String(
624                operand[1..operand.len() - 1].to_string(),
625            ))
626        } else if let Ok(num) = operand.parse::<i64>() {
627            // Integer
628            Ok(serde_json::Value::Number(num.into()))
629        } else if let Ok(num) = operand.parse::<f64>() {
630            // Float
631            Ok(serde_json::json!(num))
632        } else if operand == "true" {
633            Ok(serde_json::Value::Bool(true))
634        } else if operand == "false" {
635            Ok(serde_json::Value::Bool(false))
636        } else {
637            // Try as key in data
638            Ok(data
639                .get(operand)
640                .cloned()
641                .unwrap_or_else(|| serde_json::Value::String(operand.to_string())))
642        }
643    }
644
645    fn evaluate_constraint_type(
646        &self,
647        ctype: ConstraintType,
648        left: &serde_json::Value,
649        right: Option<&serde_json::Value>,
650        operator_value: Option<&str>,
651    ) -> Result<bool, String> {
652        match ctype {
653            ConstraintType::Equality => Ok(right == Some(left)),
654            ConstraintType::Inequality => Ok(right != Some(left)),
655            ConstraintType::Greater => {
656                if let (Some(l), Some(r)) = (left.as_f64(), right.and_then(|v| v.as_f64())) {
657                    Ok(l > r)
658                } else {
659                    Err("Cannot compare non-numeric values".to_string())
660                }
661            }
662            ConstraintType::Less => {
663                if let (Some(l), Some(r)) = (left.as_f64(), right.and_then(|v| v.as_f64())) {
664                    Ok(l < r)
665                } else {
666                    Err("Cannot compare non-numeric values".to_string())
667                }
668            }
669            ConstraintType::Contains => {
670                if let Some(r) = right {
671                    if let Some(arr) = r.as_array() {
672                        Ok(arr.contains(left))
673                    } else if let Some(obj) = r.as_object() {
674                        Ok(obj.contains_key(left.as_str().unwrap_or("")))
675                    } else {
676                        Ok(false)
677                    }
678                } else {
679                    Ok(false)
680                }
681            }
682            ConstraintType::Matches => {
683                if let Some(pattern) = operator_value {
684                    if let Some(s) = left.as_str() {
685                        // Simple substring match for now (full regex would require regex crate)
686                        Ok(s.contains(pattern))
687                    } else {
688                        Ok(false)
689                    }
690                } else {
691                    Ok(false)
692                }
693            }
694            ConstraintType::TypeCheck => {
695                if let Some(expected_type) = operator_value {
696                    let matches = match expected_type.to_lowercase().as_str() {
697                        "str" | "string" => left.is_string(),
698                        "int" | "integer" => {
699                            left.is_number()
700                                && left.as_f64().unwrap_or(0.0).fract().abs() < f64::EPSILON
701                        }
702                        "float" | "number" => left.is_number(),
703                        "bool" | "boolean" => left.is_boolean(),
704                        "array" | "list" => left.is_array(),
705                        "object" | "dict" => left.is_object(),
706                        _ => false,
707                    };
708                    Ok(matches)
709                } else {
710                    Ok(false)
711                }
712            }
713            ConstraintType::Range => {
714                if let Some(range_str) = operator_value {
715                    if let Some((min_str, max_str)) = range_str.split_once(',') {
716                        if let (Ok(min_val), Ok(max_val), Some(val)) = (
717                            min_str.trim().parse::<f64>(),
718                            max_str.trim().parse::<f64>(),
719                            left.as_f64(),
720                        ) {
721                            Ok(val >= min_val && val <= max_val)
722                        } else {
723                            Err("Invalid range format".to_string())
724                        }
725                    } else {
726                        Err("Range must be in format 'min,max'".to_string())
727                    }
728                } else {
729                    Ok(false)
730                }
731            }
732            ConstraintType::Custom => {
733                if let Some(pred_name) = operator_value {
734                    if let Some(predicate) = self.custom_predicates.get(pred_name) {
735                        Ok(predicate(left, right))
736                    } else {
737                        Err(format!("Unknown custom predicate: {}", pred_name))
738                    }
739                } else {
740                    Err("Custom constraint requires operator_value".to_string())
741                }
742            }
743        }
744    }
745}
746
747impl Default for ConstraintEvaluator {
748    fn default() -> Self {
749        Self::new()
750    }
751}
752
753// =============================================================================
754// Inference Engine
755// =============================================================================
756
757/// Forward-chaining inference engine
758pub struct InferenceEngine {
759    /// Maximum iterations
760    max_iterations: usize,
761    /// Detect contradictions? (reserved for future use)
762    #[allow(dead_code)]
763    detect_contradictions: bool,
764    /// Rules
765    rules: Vec<InferenceRule>,
766    /// Facts
767    facts: HashMap<String, LogicalFact>,
768    /// Evaluator
769    evaluator: ConstraintEvaluator,
770}
771
772impl InferenceEngine {
773    /// Create a new inference engine
774    pub fn new(max_iterations: usize, detect_contradictions: bool) -> Self {
775        Self {
776            max_iterations,
777            detect_contradictions,
778            rules: Vec::new(),
779            facts: HashMap::new(),
780            evaluator: ConstraintEvaluator::new(),
781        }
782    }
783
784    /// Add a rule
785    pub fn add_rule(&mut self, rule: InferenceRule) {
786        self.rules.push(rule);
787        // Sort by priority (higher first)
788        self.rules.sort_by(|a, b| b.priority.cmp(&a.priority));
789    }
790
791    /// Add a fact
792    pub fn add_fact(&mut self, fact: LogicalFact) {
793        self.facts.insert(fact.fact_id.clone(), fact);
794    }
795
796    /// Assert a new fact
797    pub fn assert_fact(&mut self, statement: &str, confidence: f64) -> LogicalFact {
798        let fact_id = format!("fact_{}", self.facts.len());
799        let fact = LogicalFact::new(&fact_id, statement, confidence);
800        self.facts.insert(fact_id.clone(), fact.clone());
801        fact
802    }
803
804    /// Run forward-chaining inference
805    pub fn infer(&mut self, data: &serde_json::Value) -> Vec<LogicalFact> {
806        let mut derived = Vec::new();
807        let mut iteration = 0;
808
809        while iteration < self.max_iterations {
810            let mut new_facts = Vec::new();
811
812            for rule in &self.rules {
813                let result = self.apply_rule(rule, data);
814                if result.premises_satisfied {
815                    for conclusion in &result.conclusions_derived {
816                        let fact_id = format!("derived_{}", self.facts.len() + new_facts.len());
817                        let fact = LogicalFact::derived(&fact_id, conclusion, &rule.rule_id);
818                        new_facts.push(fact);
819                    }
820                }
821            }
822
823            if new_facts.is_empty() {
824                break;
825            }
826
827            // Add new facts
828            for fact in &new_facts {
829                self.facts.insert(fact.fact_id.clone(), fact.clone());
830                derived.push(fact.clone());
831            }
832
833            iteration += 1;
834        }
835
836        derived
837    }
838
839    fn apply_rule(&self, rule: &InferenceRule, data: &serde_json::Value) -> RuleValidationResult {
840        let mut premise_results = Vec::new();
841        let mut all_satisfied = true;
842
843        for premise in &rule.premises {
844            let result = self.evaluator.evaluate(premise, data);
845            premise_results.push(result.clone());
846
847            match rule.combine_with {
848                LogicalOperator::And => {
849                    if result.result != ValidationResult::Valid {
850                        all_satisfied = false;
851                        break;
852                    }
853                }
854                LogicalOperator::Or => {
855                    if result.result == ValidationResult::Valid {
856                        all_satisfied = true;
857                        break;
858                    } else {
859                        all_satisfied = false;
860                    }
861                }
862                _ => {
863                    // For other operators, default to AND behavior
864                    if result.result != ValidationResult::Valid {
865                        all_satisfied = false;
866                    }
867                }
868            }
869        }
870
871        let conclusions = if all_satisfied {
872            rule.conclusions.clone()
873        } else {
874            Vec::new()
875        };
876
877        RuleValidationResult {
878            rule: rule.clone(),
879            premises_satisfied: all_satisfied,
880            premise_results,
881            conclusions_derived: conclusions,
882        }
883    }
884}
885
886// =============================================================================
887// Contradiction Detector
888// =============================================================================
889
890/// Detects logical contradictions in facts and reasoning
891pub struct ContradictionDetector {
892    /// Contradiction patterns (pattern_a, pattern_b, description)
893    contradiction_patterns: Vec<(String, String, String)>,
894}
895
896impl ContradictionDetector {
897    /// Create a new contradiction detector
898    pub fn new() -> Self {
899        Self {
900            contradiction_patterns: vec![
901                (
902                    "is true".to_string(),
903                    "is false".to_string(),
904                    "Direct truth contradiction".to_string(),
905                ),
906                (
907                    "exists".to_string(),
908                    "does not exist".to_string(),
909                    "Existence contradiction".to_string(),
910                ),
911                (
912                    "is valid".to_string(),
913                    "is invalid".to_string(),
914                    "Validity contradiction".to_string(),
915                ),
916                (
917                    "should".to_string(),
918                    "should not".to_string(),
919                    "Normative contradiction".to_string(),
920                ),
921                (
922                    "must".to_string(),
923                    "must not".to_string(),
924                    "Obligation contradiction".to_string(),
925                ),
926                (
927                    "always".to_string(),
928                    "never".to_string(),
929                    "Temporal contradiction".to_string(),
930                ),
931                (
932                    "all".to_string(),
933                    "none".to_string(),
934                    "Quantifier contradiction".to_string(),
935                ),
936            ],
937        }
938    }
939
940    /// Detect contradictions among facts
941    pub fn detect(&self, facts: &[LogicalFact]) -> Vec<ContradictionInfo> {
942        let mut contradictions = Vec::new();
943        let statements: Vec<(String, String)> = facts
944            .iter()
945            .map(|f| (f.fact_id.clone(), f.statement.to_lowercase()))
946            .collect();
947
948        for (i, (id_a, stmt_a)) in statements.iter().enumerate() {
949            for (id_b, stmt_b) in statements.iter().skip(i + 1) {
950                if let Some(description) = self.check_contradiction(stmt_a, stmt_b) {
951                    contradictions.push(ContradictionInfo {
952                        contradiction_id: format!("contradiction_{}", contradictions.len()),
953                        description,
954                        fact_a: id_a.clone(),
955                        fact_b: id_b.clone(),
956                        source_rule: None,
957                        source_constraint: None,
958                        resolved: false,
959                        resolution_method: None,
960                        resolution_fact: None,
961                    });
962                }
963            }
964        }
965
966        contradictions
967    }
968
969    fn check_contradiction(&self, stmt_a: &str, stmt_b: &str) -> Option<String> {
970        for (pattern_a, pattern_b, description) in &self.contradiction_patterns {
971            if ((stmt_a.contains(pattern_a) && stmt_b.contains(pattern_b))
972                || (stmt_a.contains(pattern_b) && stmt_b.contains(pattern_a)))
973                && self.same_subject(stmt_a, stmt_b)
974            {
975                return Some(description.clone());
976            }
977        }
978        None
979    }
980
981    fn same_subject(&self, stmt_a: &str, stmt_b: &str) -> bool {
982        let words_a: std::collections::HashSet<&str> = stmt_a.split_whitespace().collect();
983        let words_b: std::collections::HashSet<&str> = stmt_b.split_whitespace().collect();
984
985        let common: std::collections::HashSet<&str> =
986            ["the", "a", "an", "is", "are", "was", "were", "be", "been"]
987                .iter()
988                .cloned()
989                .collect();
990
991        let words_a: std::collections::HashSet<&str> =
992            words_a.difference(&common).cloned().collect();
993        let words_b: std::collections::HashSet<&str> =
994            words_b.difference(&common).cloned().collect();
995
996        if words_a.is_empty() || words_b.is_empty() {
997            return false;
998        }
999
1000        let overlap = words_a.intersection(&words_b).count();
1001        let min_len = words_a.len().min(words_b.len());
1002        overlap as f64 / min_len as f64 > 0.3
1003    }
1004}
1005
1006impl Default for ContradictionDetector {
1007    fn default() -> Self {
1008        Self::new()
1009    }
1010}
1011
1012// =============================================================================
1013// Deep Logic Validator (Main Interface)
1014// =============================================================================
1015
1016/// Main neuro-symbolic validation system
1017pub struct DeepLogicValidator {
1018    /// Constraints to validate
1019    constraints: Vec<LogicalConstraint>,
1020    /// Inference engine
1021    inference_engine: InferenceEngine,
1022    /// Constraint evaluator
1023    evaluator: ConstraintEvaluator,
1024    /// Contradiction detector
1025    contradiction_detector: ContradictionDetector,
1026}
1027
1028impl DeepLogicValidator {
1029    /// Create a new deep logic validator
1030    pub fn new() -> Self {
1031        Self {
1032            constraints: Vec::new(),
1033            inference_engine: InferenceEngine::new(100, true),
1034            evaluator: ConstraintEvaluator::new(),
1035            contradiction_detector: ContradictionDetector::new(),
1036        }
1037    }
1038
1039    /// Add a constraint
1040    pub fn add_constraint(&mut self, constraint: LogicalConstraint) {
1041        self.constraints.push(constraint);
1042    }
1043
1044    /// Add an inference rule
1045    pub fn add_rule(&mut self, rule: InferenceRule) {
1046        self.inference_engine.add_rule(rule);
1047    }
1048
1049    /// Validate data and reasoning output
1050    pub fn validate(
1051        &mut self,
1052        data: &serde_json::Value,
1053        _reasoning_output: Option<&serde_json::Value>,
1054    ) -> DeepLogicValidation {
1055        let mut result = DeepLogicValidation::new(true);
1056
1057        // Evaluate constraints
1058        for constraint in &self.constraints {
1059            let constraint_result = self.evaluator.evaluate(constraint, data);
1060            result.constraint_results.push(constraint_result.clone());
1061
1062            match constraint_result.result {
1063                ValidationResult::Valid => {
1064                    result.constraints_satisfied += 1;
1065                }
1066                ValidationResult::Invalid => {
1067                    result.constraints_violated += 1;
1068                    if constraint.is_required {
1069                        result.is_valid = false;
1070                        result.errors.push(constraint_result.error_message);
1071                    }
1072                }
1073                _ => {
1074                    result.warnings.push(format!(
1075                        "Constraint {} could not be evaluated",
1076                        constraint.constraint_id
1077                    ));
1078                }
1079            }
1080        }
1081
1082        // Run inference
1083        let derived_facts = self.inference_engine.infer(data);
1084        result.facts_derived = derived_facts.clone();
1085        result.rules_applied = self.inference_engine.rules.len();
1086
1087        // Detect contradictions
1088        let all_facts: Vec<LogicalFact> = self.inference_engine.facts.values().cloned().collect();
1089        let contradictions = self.contradiction_detector.detect(&all_facts);
1090        result.contradictions = contradictions.clone();
1091        result.has_contradictions = !contradictions.is_empty();
1092
1093        if result.has_contradictions {
1094            result.is_valid = false;
1095            result
1096                .errors
1097                .push("Contradictions detected in reasoning".to_string());
1098        }
1099
1100        // Calculate confidence
1101        let total_constraints = result.constraints_satisfied + result.constraints_violated;
1102        if total_constraints > 0 {
1103            result.confidence = result.constraints_satisfied as f64 / total_constraints as f64;
1104        }
1105
1106        result
1107    }
1108}
1109
1110impl Default for DeepLogicValidator {
1111    fn default() -> Self {
1112        Self::new()
1113    }
1114}
1115
1116#[cfg(test)]
1117mod tests {
1118    use super::*;
1119
1120    #[test]
1121    fn test_constraint_equality() {
1122        let constraint = LogicalConstraint::equality("age", "18", "Age must be 18");
1123        assert_eq!(constraint.constraint_type, ConstraintType::Equality);
1124        assert_eq!(constraint.left_operand, "age");
1125        assert_eq!(constraint.right_operand, Some("18".to_string()));
1126    }
1127
1128    #[test]
1129    fn test_constraint_display() {
1130        let constraint = LogicalConstraint::equality("x", "y", "Test");
1131        assert!(constraint.to_string().contains("=="));
1132    }
1133
1134    #[test]
1135    fn test_inference_rule() {
1136        let rule = InferenceRule::new("test_rule")
1137            .with_name("Test Rule")
1138            .with_premise(LogicalConstraint::greater("age", "17", "Must be adult"))
1139            .with_conclusion("is_adult")
1140            .with_priority(10);
1141
1142        assert_eq!(rule.rule_id, "test_rule");
1143        assert_eq!(rule.name, "Test Rule");
1144        assert_eq!(rule.premises.len(), 1);
1145        assert_eq!(rule.conclusions.len(), 1);
1146        assert_eq!(rule.priority, 10);
1147    }
1148
1149    #[test]
1150    fn test_constraint_evaluator_equality() {
1151        let evaluator = ConstraintEvaluator::new();
1152        let constraint = LogicalConstraint::equality("age", "18", "Age must be 18");
1153        let data = serde_json::json!({ "age": 18 });
1154
1155        let result = evaluator.evaluate(&constraint, &data);
1156        assert_eq!(result.result, ValidationResult::Valid);
1157    }
1158
1159    #[test]
1160    fn test_constraint_evaluator_greater() {
1161        let evaluator = ConstraintEvaluator::new();
1162        let constraint = LogicalConstraint::greater("age", "17", "Must be adult");
1163        let data = serde_json::json!({ "age": 18 });
1164
1165        let result = evaluator.evaluate(&constraint, &data);
1166        assert_eq!(result.result, ValidationResult::Valid);
1167    }
1168
1169    #[test]
1170    fn test_inference_engine() {
1171        let mut engine = InferenceEngine::new(10, false);
1172        let rule = InferenceRule::new("adult_rule")
1173            .with_premise(LogicalConstraint::greater("age", "17", "Must be adult"))
1174            .with_conclusion("is_adult");
1175
1176        engine.add_rule(rule);
1177        let data = serde_json::json!({ "age": 18 });
1178        let derived = engine.infer(&data);
1179
1180        assert!(!derived.is_empty());
1181        assert!(derived[0].statement == "is_adult");
1182    }
1183
1184    #[test]
1185    fn test_contradiction_detector() {
1186        let detector = ContradictionDetector::new();
1187        let facts = vec![
1188            LogicalFact::new("f1", "X is true", 1.0),
1189            LogicalFact::new("f2", "X is false", 1.0),
1190        ];
1191
1192        let contradictions = detector.detect(&facts);
1193        assert!(!contradictions.is_empty());
1194    }
1195
1196    #[test]
1197    fn test_deep_logic_validator() {
1198        let mut validator = DeepLogicValidator::new();
1199        validator.add_constraint(LogicalConstraint::equality("age", "18", "Age must be 18"));
1200
1201        let data = serde_json::json!({ "age": 18 });
1202        let result = validator.validate(&data, None);
1203
1204        assert!(result.is_valid);
1205        assert_eq!(result.constraints_satisfied, 1);
1206    }
1207}
reasonkit/thinktool/deep_logic.rs

reasonkit/thinktool/
deep_logic.rs
