AGISystem2 is designed for applications where formal verification, complete traceability, and explicit reasoning are requirements. This page describes realistic use cases, including their limitations and trade-offs.
Honest positioning: AGISystem2 complements LLMs for specific scenarios—it does not replace them. For many applications, LLMs alone are sufficient and more practical. Use AGISystem2 when the cost of errors or unexplainability is high.
When to Use AGISystem2
Good Fit
- Decisions must be formally explainable
- Regulatory compliance is mandatory
- Audit trails are legally required
- Domain can be formalized as rules
- Consistency checking is valuable
- Errors have significant consequences
Poor Fit
- Open-ended creative tasks
- Ambiguous natural language input
- Domains that can't be formalized
- "Good enough" is acceptable
- Speed matters more than verification
- No resources for domain modeling
Capability Comparison (Nuanced)
| Capability |
LLMs |
AGISystem2 |
Trade-off |
| Pattern recognition |
Excellent |
Similarity-based only |
LLMs far superior for perception |
| Multi-step reasoning |
Emergent, hard to verify |
Explicit formal chains |
AGISystem2 requires formalization |
| Learning new facts |
Requires retraining/context |
Instant integration |
AGISystem2 doesn't generalize |
| Explaining reasoning |
Post-hoc rationalization |
Actual derivation trace |
Traces can be technical |
| Natural language |
Native capability |
Requires bridge layer |
AGISystem2 needs NL translation |
| Handling ambiguity |
Robust |
Requires disambiguation |
LLMs more flexible |
Use Case 1: Compliance Verification Research
Value proposition: Encode regulations as formal rules. Check actions before execution. Generate proof traces (audit logging/export is external).
Status: Research pattern (not shipped as runnable Core/config). Examples are illustrative; audit logging/export requires external integration.
The Scenario
Organizations face regulatory requirements (GDPR, HIPAA, internal policies) where violations have significant consequences. Current approach: periodic audits that find problems after they've occurred.
How AGISystem2 Helps
- Formal rule encoding: Regulations expressed as checkable constraints
- Pre-action validation: Operations checked before execution
- Proof traces: Every decision traceable to specific rules (audit logging/export is external)
- Remediation guidance: Not just "violation" but "here's how to fix it"
Example
Action: MarketingTeam processes CustomerEmails
Purpose: NewProductCampaign
GDPR Analysis:
✗ art6_consent: NOT SATISFIED
Existing consent: "marketing communications" (2023-06-01)
Required: Consent specific to NewProductCampaign
Required remediation:
Option A: Obtain specific consent
Option B: Complete Legitimate Interest Assessment
Trade-off: Requires upfront investment in formalizing regulations. Ambiguous regulatory language must be interpreted and encoded—this interpretation is a human judgment, not automatic. The system verifies against the formalization, not against "true" regulatory intent.
Compliance documentation →
Use Case 2: Agent Plan Verification Research
Value proposition: Verify AI agent plans before execution. Catch invalid plans before they cause damage.
Status: Research pattern (not shipped as runnable Core/config). Plan generation/monitoring requires external integration; AGISystem2 can model and validate semantics.
The Scenario
LLM-based agents generate action plans, but these plans may violate preconditions or have unintended effects. Failures only become apparent at execution time.
How AGISystem2 Helps
- Formal tool semantics: Each tool's preconditions and effects defined
- Pre-execution checking: Plans validated before any action runs
- Failure diagnosis: Missing preconditions explicitly identified
- Alternative generation: Valid alternatives suggested when plans fail
Example
Goal: "Send Q3 report to team"
Generated plan:
1. Login(SalesDB) ✓ Pre: HasCredentials - satisfied
2. QueryDatabase(Q3) ✓ Pre: Connected - will be satisfied
3. Login(EmailServer) ✓ Pre: HasCredentials - satisfied
4. SendEmail(Report) ✓ Pre: HasData - will be satisfied
Plan Status: VALID ✓
Trade-off: Every tool must have formally defined preconditions and effects. This works for well-defined APIs but is difficult for fuzzy real-world actions. Plan generation itself still relies on LLMs; AGISystem2 only verifies.
Agent planning documentation →
Use Case 3: Knowledge Base Reasoning Demonstrated
Value proposition: Taxonomic inference with complete traceability. Every conclusion traceable to source facts and rules.
The Scenario
Organizations need to query knowledge bases and understand exactly how answers were derived. "Why is X true?" should have a verifiable answer.
How AGISystem2 Helps
- Transitive inference: Automatic reasoning through IS_A hierarchies
- Proof traces: Complete derivation available for every query
- Contradiction detection: Inconsistencies flagged explicitly
- Incremental updates: New facts integrate without retraining
Example
Facts:
isA(Spot, Dog)
isA(Dog, Animal)
isA(Animal, LivingThing)
Query: isA(Spot, LivingThing)?
Result: TRUE
Proof:
1. isA(Spot, Dog) [direct fact]
2. isA(Dog, Animal) [direct fact]
3. isA(Animal, LivingThing) [direct fact]
4. isA(Spot, LivingThing) [transitive chain: 1→2→3]
Trade-off: Works well for taxonomies and rule-based domains. Does not handle probabilistic reasoning, fuzzy categories, or exceptions gracefully. Knowledge must be explicitly encoded—the system doesn't learn from examples.
Use Case 4: Thinking Database (RAG Alternative) Implemented
Value proposition: Replace semantic search approximations with verifiable logical reasoning.
Get real answers derived from formal proofs, not statistical similarity matches.
The Problem with RAG
Retrieval-Augmented Generation (RAG) finds "similar" documents using vector embeddings, but:
- Similarity ≠ Relevance: Semantically similar text may not contain the actual answer
- No reasoning: RAG retrieves, it doesn't think—multi-step inference is impossible
- Hallucination risk: LLM may still hallucinate even with retrieved context
- No provenance: "Where did this answer come from?" is hard to answer
The Thinking Database Approach
AGISystem2 as a "thinking database" provides:
- Logical derivation: Answers are proved, not retrieved
- Multi-step reasoning: Chains facts and rules to reach conclusions
- Formal proof trace: Every answer has a derivation trace
- Consistency guarantees: Contradictions are detected, not hidden
Comparison
| Aspect |
RAG (Semantic Search) |
Thinking Database |
| Query |
"Find similar documents" |
"Prove this is true" |
| Answer source |
Retrieved text chunks |
Logical derivation |
| Multi-step reasoning |
No (single retrieval) |
Yes (chained inference) |
| Explainability |
"These docs were similar" |
"Here's the proof" |
| Consistency |
Can return contradictions |
Contradictions detected |
Example
Question: "Can employees in the Finance department access customer data?"
RAG approach:
→ Vector search finds: "Finance handles sensitive financial data..."
→ LLM generates: "Yes, Finance can access data" (WRONG - no reasoning)
Thinking Database approach:
Knowledge Base:
- Finance department handles FinancialData
- CustomerData requires CustomerDataAccess permission
- Finance department has FinancialDataAccess permission
- CustomerDataAccess ≠ FinancialDataAccess
Query: canAccess(Finance, CustomerData)?
Result: FALSE
Proof:
1. canAccess(X, CustomerData) requires hasPermission(X, CustomerDataAccess)
2. hasPermission(Finance, FinancialDataAccess) [fact]
3. NOT hasPermission(Finance, CustomerDataAccess) [no matching fact]
4. Therefore: canAccess(Finance, CustomerData) = FALSE
Trade-off: Requires structured knowledge base (not free-form documents). Best for domains with clear rules and relationships. Can be combined with RAG: use RAG for initial retrieval, then verify with formal reasoning.
Use Case 5: LLM Output Verification Theoretical
Value proposition: Check LLM outputs against formal constraints. Catch inconsistencies and hallucinations.
The Scenario
LLMs generate content that may contain factual errors or violate domain constraints. Human review is expensive and inconsistent.
How AGISystem2 Could Help
- Constraint checking: Verify LLM outputs against known rules
- Consistency checking: Flag contradictions with established facts
- Confidence calibration: Distinguish verified from unverified claims
Conceptual Example
LLM output: "The water boiled at 50°C at standard pressure"
Knowledge base constraint:
boilingPoint(Water, StandardPressure) = 100°C
Verification result: INCONSISTENT
LLM claimed: 50°C
Known value: 100°C
Recommendation: Flag for review or reject
Trade-off: Only catches errors that contradict formalized knowledge. Novel hallucinations outside the knowledge base cannot be detected. Requires extracting structured claims from LLM text (itself error-prone). This is a research direction, not a deployed capability.
Use Case 6: Scientific Reasoning Support Theoretical
Value proposition: Encode theories formally. Check claims against established knowledge. Explore hypotheticals.
The Scenario
Scientific claims need validation against established theory. "What if?" hypotheses are difficult to explore systematically.
How AGISystem2 Could Help
- Theory encoding: Laws and constraints as formal structures
- Claim validation: New results checked for consistency
- Hypothesis exploration: "What would follow if X?"
Conceptual Example
Claim: "Our engine achieved 95% efficiency"
Operating between 300K and 400K
Theoretical check:
Carnot limit = 1 - (300/400) = 25%
Result: INCONSISTENT WITH THERMODYNAMICS
Claimed: 95%
Maximum possible: 25%
Trade-off: Requires formalizing scientific theories—a significant undertaking. Works for well-understood, rule-based domains (thermodynamics limits, conservation laws). Does not handle cutting-edge research where the rules themselves are uncertain. This is a research direction.
Implementation Reality
What's Actually Working Today
- Taxonomic inference: IS_A hierarchies with transitive reasoning (126/126 eval tests passing)
- Rule-based reasoning: Backward chaining with And/Or conditions
- Proof traces: Complete derivation history for every conclusion
- Basic NL output: DSL results converted to readable text
What's In Development
- NL→DSL translation (requires LLM bridge)
- Trustworthy AI pattern library
- Integration examples with real systems
What's Theoretical
- Large-scale deployment validation
- Complex domain formalization methodologies
- Hybrid LLM+AGISystem2 architectures
Getting Started (Realistic)
- Assess fit: Does your use case require formal verification? Is the domain formalizable?
- Scope narrowly: Start with a specific, well-defined sub-domain
- Formalize carefully: Encode domain knowledge as theories (this is the hard part)
- Validate incrementally: Test with known cases before deploying
- Maintain continuously: Theories need updating as requirements change
Related Documentation