import { LogicManager } from './logicManager.js';
import { processCommand, StandardParams } from './commandHandler.js';
import { createCommandError } from './errorHandler.js';
import { Loggers } from './utils/logger.js';
import { BatchProcessor } from './batchProcessor.js';
import { LogicTranslator } from './logicTranslator.js';
import { ContradictionDetector } from './contradictionDetector.js';
import { ProofLibrary } from './proofLibrary.js';
import { AssumptionExtractor } from './assumptionExtractor.js';
import { ArgumentScorer } from './argumentScorer.js';
import * as path from 'path';
import { fileURLToPath } from 'url';
const logger = Loggers.server;
// Get the directory of the current module
const __filename = fileURLToPath(import.meta.url);
const __dirname = path.dirname(__filename);
// JSON-RPC 2.0 types
interface JSONRPCRequest {
jsonrpc: "2.0";
method: string;
params?: any;
id?: string | number | null;
}
interface JSONRPCResponse {
jsonrpc: "2.0";
result?: any;
error?: JSONRPCError;
id: string | number | null;
}
interface JSONRPCError {
code: number;
message: string;
data?: any;
}
// Create the logic manager and batch processor instances
const logicManager = new LogicManager();
const batchProcessor = new BatchProcessor(logicManager);
const logicTranslator = new LogicTranslator(logicManager);
const contradictionDetector = new ContradictionDetector(logicManager);
// Use absolute path relative to project root (one level up from dist)
const dbPath = path.join(__dirname, '..', 'data', 'proofs.db');
const proofLibrary = new ProofLibrary(dbPath);
const assumptionExtractor = new AssumptionExtractor(logicManager);
const argumentScorer = new ArgumentScorer(logicManager, assumptionExtractor);
// Process stdin/stdout for MCP communication
process.stdin.setEncoding('utf-8');
let inputBuffer = '';
process.stdin.on('data', (chunk: string) => {
inputBuffer += chunk;
// Process complete messages (one per line)
let newlineIndex;
while ((newlineIndex = inputBuffer.indexOf('\n')) !== -1) {
const line = inputBuffer.slice(0, newlineIndex);
inputBuffer = inputBuffer.slice(newlineIndex + 1);
try {
// Parse the request as JSON-RPC
const request = JSON.parse(line) as any;
// Validate JSON-RPC format
if (request.jsonrpc !== "2.0") {
throw new Error('Invalid JSON-RPC version');
}
// Process the request (now async)
processJSONRPCRequest(request).then(result => {
// Only send a response for requests (not notifications)
if (request.id !== undefined) {
const response: JSONRPCResponse = {
jsonrpc: "2.0",
result: result,
id: request.id
};
process.stdout.write(JSON.stringify(response) + '\n');
}
}).catch(error => {
// Handle async errors properly
logger.error('Error processing async request', {
error: error instanceof Error ? error.message : String(error),
requestId: request.id,
stack: error instanceof Error ? error.stack : undefined
});
// Send error response if this was a request (not notification)
if (request.id !== undefined) {
const errorResponse: JSONRPCResponse = {
jsonrpc: "2.0",
error: {
code: (typeof error === 'object' && error !== null && 'code' in error)
? (error as any).code
: -32603,
message: error instanceof Error ? error.message : String(error),
data: error
},
id: request.id
};
process.stdout.write(JSON.stringify(errorResponse) + '\n');
}
});
} catch (error) {
logger.error('Error processing request', {
error: error instanceof Error ? error.message : String(error),
line: line.substring(0, 100) // Log first 100 chars of problematic line
});
// Send a JSON-RPC error response only if we have an id
let requestId = null;
if (line) {
try {
const parsedLine = JSON.parse(line);
requestId = parsedLine.id;
} catch {}
}
const errorResponse: JSONRPCResponse = {
jsonrpc: "2.0",
error: {
code: -32603, // Internal error
message: error instanceof Error ? error.message : 'Internal error',
data: error
},
id: requestId
};
process.stdout.write(JSON.stringify(errorResponse) + '\n');
}
}
});
/**
* Process a JSON-RPC request
* @param request The JSON-RPC request
* @returns Logic result
*/
async function processJSONRPCRequest(request: JSONRPCRequest) {
const { method, params } = request;
// Handle MCP methods
switch (method) {
case 'initialize':
return handleInitialize(params);
case 'initialized':
case 'notifications/initialized':
// Just handle the notification silently
return null;
case 'tools/list':
return handleListTools(params);
case 'resources/list':
// Return empty resources list
return { resources: [] };
case 'tools/call':
return await handleToolCall(params);
case 'ping':
return handlePing(params);
default:
throw {
code: -32601, // Method not found
message: `Method not found: ${method}`
};
}
}
/**
* Handle initialize request
*/
function handleInitialize(params: any) {
return {
protocolVersion: "2024-11-05",
capabilities: {
tools: {},
logging: {}
},
serverInfo: {
name: "logic-thinking",
version: "0.1.0"
}
};
}
/**
* Handle list tools request
*/
function handleListTools(params: any) {
return {
tools: [
{
name: "logic-thinking",
description: `A tool for formal logical reasoning, verification, and proof construction.
Supports multiple logical systems:
- Syllogistic logic (term-based reasoning)
- Propositional logic (truth-functional reasoning)
- Predicate logic (quantified statements)
- Mathematical logic (arithmetic and sequences)
- Modal logic (necessity and possibility)
- Temporal logic (time-based reasoning)
- Fuzzy logic (degrees of truth)
- Deontic logic (obligations and permissions)
Features:
- Analyzing logical arguments for validity
- Identifying logical fallacies
- Constructing proofs
- Visualizing logical relationships
- Converting natural language to formal notation
- Performance caching for repeated queries
Commands:
- validate: Check a logical argument for validity
- formalize: Convert natural language to logical notation
- visualize: Create a visualization of logical relationships
- solve: Find a solution or proof for a logical problem
- score: Score argument strength on multiple dimensions (validity, plausibility, inference, structure, fallacies, assumptions)
- help: Display help information and examples
- listSystems: List available logical systems
- listOperations: List available operations
- listFallacies: List common logical fallacies
- showExamples: Show examples for specific systems or operations
- cacheStats: Show cache performance statistics
- clearCache: Clear the cache`,
inputSchema: {
type: "object",
properties: {
system: {
type: "string",
enum: ["syllogistic", "propositional", "predicate", "mathematical", "modal", "temporal", "fuzzy", "deontic", "auto"],
description: "The logical system to use"
},
operation: {
type: "string",
enum: ["validate", "formalize", "visualize", "solve", "score"],
description: "The operation to perform"
},
input: {
type: "string",
description: "The logical statement or problem to analyze"
},
format: {
type: "string",
enum: ["natural", "symbolic", "mixed"],
description: "Input format (natural language, symbolic notation, or mixed)"
},
additionalContext: {
type: "string",
description: "Optional additional context or constraints"
},
command: {
type: "object",
description: "Optional command for special operations",
properties: {
type: {
type: "string",
enum: ["help", "listSystems", "listOperations", "listFallacies", "showHistory", "exportProof", "showExamples", "cacheStats", "clearCache"],
description: "Command type"
},
parameters: {
type: "object",
description: "Command parameters"
}
},
required: ["type"]
}
},
required: ["system", "operation", "input", "format"]
}
},
{
name: "logic-batch",
description: `Batch processing tool for multiple logic operations at once.
Process multiple logical arguments, validations, or operations concurrently for improved throughput.
Useful for:
- Validating multiple arguments simultaneously
- Processing sets of related logic problems
- Batch proof generation
- Performance testing
Features:
- Concurrent or sequential processing
- Per-request result tracking with IDs
- Fail-fast or continue-on-error modes
- Comprehensive batch statistics
- Safety limits (max 50 requests per batch)`,
inputSchema: {
type: "object",
properties: {
requests: {
type: "array",
description: "Array of logic requests to process",
items: {
type: "object",
properties: {
id: {
type: "string",
description: "Optional unique identifier for this request"
},
system: {
type: "string",
enum: ["syllogistic", "propositional", "predicate", "mathematical", "modal", "temporal", "fuzzy", "deontic", "auto"],
description: "The logical system to use"
},
operation: {
type: "string",
enum: ["validate", "formalize", "visualize", "solve"],
description: "The operation to perform"
},
input: {
type: "string",
description: "The logical statement or problem"
},
format: {
type: "string",
enum: ["natural", "symbolic", "mixed"],
description: "Input format"
},
additionalContext: {
type: "string",
description: "Optional additional context"
}
},
required: ["system", "operation", "input"]
}
},
options: {
type: "object",
description: "Batch processing options",
properties: {
concurrent: {
type: "boolean",
description: "Process requests concurrently (default: false)"
},
failFast: {
type: "boolean",
description: "Stop on first error (default: false)"
},
maxConcurrent: {
type: "number",
description: "Max concurrent requests (default: 10, max: 10)"
}
}
}
},
required: ["requests"]
}
},
{
name: "logic-translate",
description: `Cross-system logic translation tool.
Translate logical statements between different formal systems.
Supports 7 translation pairs with automatic limitation tracking.
Translation Pairs:
- Propositional → Modal (lossless)
- Propositional → Predicate (lossless)
- Syllogistic → Predicate (lossless)
- Modal → Propositional (lossy: strips modalities)
- Predicate → Propositional (lossy: removes quantifiers)
- Temporal → Modal (lossless: G→□, F→◇)
- Fuzzy → Propositional (lossy: threshold binarization)
Features:
- Automatic formalization in source system
- Lossless vs lossy translation tracking
- Detailed translation notes
- Limitation warnings for lossy translations`,
inputSchema: {
type: "object",
properties: {
input: {
type: "string",
description: "The logical statement to translate"
},
sourceSystem: {
type: "string",
enum: ["syllogistic", "propositional", "predicate", "modal", "temporal", "fuzzy"],
description: "Source logical system"
},
targetSystem: {
type: "string",
enum: ["propositional", "predicate", "modal"],
description: "Target logical system"
}
},
required: ["input", "sourceSystem", "targetSystem"]
}
},
{
name: "logic-contradiction",
description: `Contradiction detection tool for sets of logical statements.
Detect contradictions in statement sets with three severity levels.
Find maximal consistent subsets and get actionable recommendations.
Severity Levels:
- Direct: Syntactic contradictions (A and ¬A)
- Logical: Semantic contradictions (joint entailment of false)
- Contextual: Domain-specific contradictions
Features:
- Multi-statement consistency checking
- Pairwise contradiction detection
- Maximal consistent subset identification
- Actionable recommendations for resolution
- Support for propositional, predicate, and modal systems`,
inputSchema: {
type: "object",
properties: {
statements: {
type: "array",
description: "Array of logical statements to check for contradictions",
items: {
type: "string"
}
},
system: {
type: "string",
enum: ["propositional", "predicate", "modal"],
description: "Logical system to use for checking (default: propositional)",
default: "propositional"
}
},
required: ["statements"]
}
},
{
name: "logic-proof-save",
description: `Save a logical proof to the library for future reuse.
Store proofs with metadata for easy retrieval and composition.
Supports all logic systems and includes usage tracking.
Features:
- Save proofs with descriptive names and tags
- Track authorship (user or claude)
- Automatic usage counting and success rate tracking
- Full-text search indexing
- Support for all 8 logical systems`,
inputSchema: {
type: "object",
properties: {
name: {
type: "string",
description: "A descriptive name for the proof"
},
description: {
type: "string",
description: "Optional detailed description of the proof"
},
system: {
type: "string",
enum: ["syllogistic", "propositional", "predicate", "mathematical", "modal", "temporal", "fuzzy", "deontic"],
description: "The logical system used in the proof"
},
premises: {
type: "array",
description: "Array of premise statements",
items: {
type: "string"
}
},
conclusion: {
type: "string",
description: "The conclusion statement"
},
proofSteps: {
type: "array",
description: "Array of proof steps",
items: {
type: "object",
properties: {
stepNumber: { type: "number" },
statement: { type: "string" },
justification: { type: "string" },
rule: { type: "string" },
references: {
type: "array",
items: { type: "number" }
}
},
required: ["stepNumber", "statement", "justification"]
}
},
tags: {
type: "array",
description: "Optional tags for categorization",
items: {
type: "string"
}
},
author: {
type: "string",
enum: ["user", "claude"],
description: "Author of the proof (default: user)",
default: "user"
},
formalizedInput: {
type: "string",
description: "Optional formalized representation"
}
},
required: ["name", "system", "premises", "conclusion", "proofSteps"]
}
},
{
name: "logic-proof-search",
description: `Search for proofs in the library.
Full-text search with filtering by system, tags, author, and success rate.
Supports multiple sorting options for optimal retrieval.
Features:
- Full-text search across names, descriptions, premises, and conclusions
- Filter by logical system, tags, author
- Sort by relevance, usage, date, or success rate
- Pagination support`,
inputSchema: {
type: "object",
properties: {
query: {
type: "string",
description: "Search query (searches names, descriptions, premises, conclusions)"
},
system: {
type: "string",
enum: ["syllogistic", "propositional", "predicate", "mathematical", "modal", "temporal", "fuzzy", "deontic"],
description: "Filter by logical system"
},
tags: {
type: "array",
description: "Filter by tags (must match all provided tags)",
items: {
type: "string"
}
},
author: {
type: "string",
enum: ["user", "claude"],
description: "Filter by author"
},
minSuccessRate: {
type: "number",
description: "Minimum success rate (0-1)"
},
limit: {
type: "number",
description: "Maximum number of results (default: 20)",
default: 20
},
offset: {
type: "number",
description: "Offset for pagination (default: 0)",
default: 0
},
sortBy: {
type: "string",
enum: ["relevance", "usage", "date", "success_rate"],
description: "Sort results by (default: relevance)",
default: "relevance"
},
sortOrder: {
type: "string",
enum: ["asc", "desc"],
description: "Sort order (default: desc)",
default: "desc"
}
}
}
},
{
name: "logic-proof-get",
description: `Retrieve a specific proof by ID.
Get complete proof details including all metadata, steps, and usage statistics.`,
inputSchema: {
type: "object",
properties: {
proofId: {
type: "string",
description: "The unique ID of the proof to retrieve"
}
},
required: ["proofId"]
}
},
{
name: "logic-proof-list",
description: `List all proofs with optional filtering.
Get a paginated list of all proofs in the library, optionally filtered by logical system.`,
inputSchema: {
type: "object",
properties: {
system: {
type: "string",
enum: ["syllogistic", "propositional", "predicate", "mathematical", "modal", "temporal", "fuzzy", "deontic"],
description: "Filter by logical system"
},
limit: {
type: "number",
description: "Maximum number of results (default: 50)",
default: 50
},
offset: {
type: "number",
description: "Offset for pagination (default: 0)",
default: 0
}
}
}
},
{
name: "logic-proof-stats",
description: `Get statistics about the proof library.
View comprehensive statistics including:
- Total proofs and lemmas
- Proofs by logical system
- Most used proofs
- Average success rate
- Proofs by author
- Recent proofs`,
inputSchema: {
type: "object",
properties: {}
}
},
{
name: "logic-extract-assumptions",
description: `Extract and analyze hidden assumptions in logical arguments.
Identifies implicit premises, background knowledge, and logical gaps that are assumed
but not explicitly stated. Provides Socratic analysis to strengthen arguments.
Detection Methods:
- Pattern-based extraction (causal, normative, definitional patterns)
- Validity gap analysis (missing premises for logical validity)
- Term extraction (equivocation and ambiguity detection)
- Background knowledge identification
Assumption Types:
- Hidden Premise: Missing premise required for validity
- Background Knowledge: Domain-specific knowledge assumed
- Definitional: Assumed definitions or meanings
- Causal: Causal relationships assumed
- Normative: Value judgments or norms assumed
- Existential: Existence assumptions
Features:
- Confidence scoring for each assumption
- Necessity classification (required/supporting/contextual)
- Validity gap identification
- Argument strength assessment
- Actionable recommendations`,
inputSchema: {
type: "object",
properties: {
premises: {
type: "array",
description: "Array of explicit premises in the argument",
items: {
type: "string"
}
},
conclusion: {
type: "string",
description: "The conclusion of the argument"
},
system: {
type: "string",
enum: ["propositional", "predicate", "modal", "syllogistic"],
description: "Logical system to use for validity checking (default: propositional)",
default: "propositional"
}
},
required: ["premises", "conclusion"]
}
}
]
};
}
/**
* Handle tool call request
*/
async function handleToolCall(params: any) {
const { name, arguments: args } = params;
// Check if arguments exist
if (!args) {
throw {
code: -32602, // Invalid params
message: 'Missing arguments property in tool call'
};
}
// Handle batch processing tool
if (name === "logic-batch") {
return await handleBatchToolCall(args);
}
// Handle translation tool
if (name === "logic-translate") {
return await handleTranslateToolCall(args);
}
// Handle contradiction detection tool
if (name === "logic-contradiction") {
return await handleContradictionToolCall(args);
}
// Handle proof library tools
if (name === "logic-proof-save") {
return handleProofSaveToolCall(args);
}
if (name === "logic-proof-search") {
return handleProofSearchToolCall(args);
}
if (name === "logic-proof-get") {
return handleProofGetToolCall(args);
}
if (name === "logic-proof-list") {
return handleProofListToolCall(args);
}
if (name === "logic-proof-stats") {
return handleProofStatsToolCall(args);
}
// Handle assumption extraction tool
if (name === "logic-extract-assumptions") {
return await handleAssumptionExtractionToolCall(args);
}
// Ensure the tool name is correct for single operations
if (name !== "logic-thinking") {
throw {
code: -32602, // Invalid params
message: `Invalid tool name: ${name}. Expected: logic-thinking, logic-batch, logic-translate, logic-contradiction, logic-proof-*, or logic-extract-assumptions`
};
}
// Check if this is a command
if (args.command) {
return processRPCCommand(args.command);
}
// Extract operation from args instead of using tool name
const system = args.system || 'auto';
const operation = args.operation;
const input = args.input;
const format = args.format || 'natural';
const additionalContext = args.additionalContext;
if (!input || !operation) {
throw {
code: -32602, // Invalid params
message: 'Missing required parameter: input or operation'
};
}
// Handle score operation specially
if (operation === 'score') {
return await handleScoreOperation(input, system, format);
}
// Reset modal system to default K before each call to prevent state persistence
if (system === 'modal') {
logicManager.setModalSystem('K');
}
// Handle additionalContext for modal systems
if (system === 'modal' && additionalContext) {
// Try to extract modal system from additionalContext
// Support formats like "system: T", "System T", "system:B", etc.
const modalSystemMatch = additionalContext.match(/system[:\s]+([A-Z0-9]+)/i);
if (modalSystemMatch) {
const requestedSystem = modalSystemMatch[1].toUpperCase();
// Validate it's a supported modal system
const validSystems = ['K', 'T', 'D', 'B', 'K4', 'KB', 'S4', 'S5', 'KD45'];
if (validSystems.includes(requestedSystem)) {
logicManager.setModalSystem(requestedSystem as any);
logger.debug(`Modal system set to ${requestedSystem} via additionalContext`);
}
}
}
try {
// Process with the logic manager
const result = await logicManager.process(system, operation, input, format, additionalContext);
// Build comprehensive response text
let responseText = result.message;
// Add details based on what's available
if (result.details) {
if (result.details.analysis) {
responseText += '\n\n' + result.details.analysis.explanation;
if (result.details.analysis.counterexample) {
responseText += '\n\nCounterexample: ' + result.details.analysis.counterexample;
}
if (result.details.analysis.fallacies && result.details.analysis.fallacies.length > 0) {
responseText += '\n\nFallacies detected:';
for (const fallacy of result.details.analysis.fallacies) {
responseText += `\n• ${fallacy.name}: ${fallacy.description} (at ${fallacy.location})`;
}
}
}
if (result.details.solution) {
responseText += '\n\nSolution:';
for (const step of result.details.solution.steps) {
responseText += `\n${step.index}. ${step.statement} (${step.rule})`;
if (step.justification) {
responseText += `\n Justification: ${step.justification}`;
}
}
responseText += `\n\nConclusion: ${result.details.solution.conclusion}`;
}
if (result.details.visualization) {
responseText += '\n\n' + result.details.visualization;
}
if (result.details.formalizedInput) {
responseText += '\n\nFormalized: ' + result.details.formalizedInput;
}
}
// Format for MCP tool response
return {
content: [
{
type: "text",
text: responseText
}
],
isError: result.status === 'error'
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Unknown error occurred';
// Provide detailed error information
let fullErrorText = errorMessage;
// Try to enhance the error message with context
if (error instanceof Error && error.message.includes('Unexpected token')) {
fullErrorText = `${errorMessage}\n\nNote: For propositional logic, use single-letter variables or valid expressions like:\n• P and Q\n• rain implies wet\n• (P or Q) implies R`;
}
return {
content: [
{
type: "text",
text: fullErrorText
}
],
isError: true
};
}
}
/**
* Handle batch processing tool call
*/
async function handleBatchToolCall(args: any) {
try {
const { requests, options } = args;
if (!requests || !Array.isArray(requests)) {
throw new Error('Missing or invalid requests array');
}
// Process the batch
const summary = await batchProcessor.processBatch(requests, options || {});
// Format results for MCP response
let responseText = `Batch Processing Complete\n\n`;
responseText += `Total: ${summary.total}\n`;
responseText += `Successful: ${summary.successful}\n`;
responseText += `Failed: ${summary.failed}\n`;
responseText += `Total Time: ${summary.totalTime}ms\n`;
responseText += `Average Time: ${summary.averageTime.toFixed(2)}ms\n\n`;
// Add individual results
responseText += `Results:\n`;
for (const result of summary.results) {
const id = result.id ? `[${result.id}] ` : '';
if (result.success && result.result) {
responseText += `\n${id}✓ ${result.result.message} (${result.processingTime}ms)`;
} else {
responseText += `\n${id}✗ ${result.error} (${result.processingTime}ms)`;
}
}
return {
content: [
{
type: "text",
text: responseText
}
],
isError: false
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Batch processing error';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Handle translation tool call
*/
async function handleTranslateToolCall(args: any) {
try {
const { input, sourceSystem, targetSystem } = args;
if (!input || !sourceSystem || !targetSystem) {
throw new Error('Missing required parameters: input, sourceSystem, or targetSystem');
}
// Perform the translation
const result = await logicTranslator.translate(input, sourceSystem, targetSystem);
// Format results for MCP response
let responseText = `Logic Translation\n\n`;
responseText += `Source System: ${result.sourceSystem}\n`;
responseText += `Target System: ${result.targetSystem}\n`;
responseText += `Status: ${result.successful ? 'Success' : 'Failed'}\n\n`;
if (result.successful) {
responseText += `Original: ${result.sourceInput}\n`;
responseText += `Translated: ${result.translatedOutput}\n`;
if (result.notes) {
responseText += `\nNotes: ${result.notes}`;
}
if (result.limitations && result.limitations.length > 0) {
responseText += `\n\nLimitations:`;
for (const limitation of result.limitations) {
responseText += `\n• ${limitation}`;
}
}
} else {
responseText += `Error: ${result.notes || 'Translation failed'}`;
}
return {
content: [
{
type: "text",
text: responseText
}
],
isError: !result.successful
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Translation error';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Handle contradiction detection tool call
*/
async function handleContradictionToolCall(args: any) {
try {
const { statements, system } = args;
if (!statements || !Array.isArray(statements)) {
throw new Error('Missing or invalid statements array');
}
const logicalSystem = system || 'propositional';
// Detect contradictions
const report = await contradictionDetector.detectContradictions(statements, logicalSystem);
// Format results for MCP response
let responseText = `Contradiction Detection Report\n\n`;
responseText += `System: ${logicalSystem}\n`;
responseText += `Statements Analyzed: ${statements.length}\n`;
responseText += `Contradictions Found: ${report.contradictions.length}\n\n`;
if (report.hasContradictions) {
responseText += `Contradictions:\n`;
for (let i = 0; i < report.contradictions.length; i++) {
const c = report.contradictions[i];
responseText += `\n${i + 1}. [${c.severity.toUpperCase()}]\n`;
responseText += ` Statement 1: "${c.statement1}"\n`;
responseText += ` Statement 2: "${c.statement2}"\n`;
responseText += ` Reason: ${c.reason}\n`;
}
if (report.consistentSubsets && report.consistentSubsets.length > 0) {
responseText += `\n\nMaximal Consistent Subsets:\n`;
for (let i = 0; i < report.consistentSubsets.length; i++) {
responseText += `\nSubset ${i + 1}:`;
for (const stmt of report.consistentSubsets[i]) {
responseText += `\n • "${stmt}"`;
}
}
}
if (report.recommendations && report.recommendations.length > 0) {
responseText += `\n\nRecommendations:\n`;
for (const rec of report.recommendations) {
responseText += `• ${rec}\n`;
}
}
} else {
responseText += `No contradictions detected. The set of statements appears consistent.`;
}
return {
content: [
{
type: "text",
text: responseText
}
],
isError: false
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Contradiction detection error';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Process a command
* @param command The command to process
* @returns Command result
*/
function processRPCCommand(command: { type: string; parameters?: any }) {
try {
// Convert to standard params format
const standardParams: StandardParams = {
command: {
type: command.type as any,
parameters: command.parameters
}
};
// Use the command handler
const result = processCommand(standardParams);
// Format for MCP tool response
return {
content: [
{
type: "text",
text: JSON.stringify(result, null, 2)
}
],
isError: false
};
} catch (error) {
// Handle error
const errorMessage = error instanceof Error ? error.message : 'Unknown command error';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Handle proof save tool call
*/
function handleProofSaveToolCall(args: any) {
try {
const { name, description, system, premises, conclusion, proofSteps, tags, author, formalizedInput } = args;
if (!name || !system || !premises || !conclusion || !proofSteps) {
throw new Error('Missing required parameters: name, system, premises, conclusion, or proofSteps');
}
// Validate premises and proofSteps are arrays
if (!Array.isArray(premises)) {
throw new Error('premises must be an array of strings');
}
if (!Array.isArray(proofSteps)) {
throw new Error('proofSteps must be an array of proof step objects');
}
// Save the proof
const savedProof = proofLibrary.saveProof(
name,
description,
system,
premises,
conclusion,
proofSteps,
tags || [],
author || 'user',
formalizedInput
);
// Format response
let responseText = `Proof Saved Successfully\n\n`;
responseText += `ID: ${savedProof.id}\n`;
responseText += `Name: ${savedProof.name}\n`;
responseText += `System: ${savedProof.system}\n`;
responseText += `Premises: ${savedProof.premises.length}\n`;
responseText += `Steps: ${savedProof.proofSteps.length}\n`;
if (savedProof.tags.length > 0) {
responseText += `Tags: ${savedProof.tags.join(', ')}\n`;
}
responseText += `\nThis proof can now be retrieved using ID: ${savedProof.id}`;
return {
content: [
{
type: "text",
text: responseText
}
],
isError: false
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Error saving proof';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Handle proof search tool call
*/
function handleProofSearchToolCall(args: any) {
try {
const results = proofLibrary.searchProofs(args);
let responseText = `Proof Search Results\n\n`;
responseText += `Found: ${results.length} proof(s)\n\n`;
if (results.length === 0) {
responseText += `No proofs found matching your criteria.`;
} else {
for (let i = 0; i < results.length; i++) {
const proof = results[i];
responseText += `${i + 1}. ${proof.name}\n`;
responseText += ` ID: ${proof.id}\n`;
responseText += ` System: ${proof.system}\n`;
responseText += ` Premises: ${proof.premises.length} | Steps: ${proof.proofSteps.length}\n`;
responseText += ` Usage: ${proof.usageCount} | Success Rate: ${(proof.successRate * 100).toFixed(1)}%\n`;
if (proof.description) {
responseText += ` Description: ${proof.description}\n`;
}
if (proof.tags.length > 0) {
responseText += ` Tags: ${proof.tags.join(', ')}\n`;
}
responseText += `\n`;
}
}
return {
content: [
{
type: "text",
text: responseText
}
],
isError: false
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Error searching proofs';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Handle proof get tool call
*/
function handleProofGetToolCall(args: any) {
try {
const { proofId } = args;
if (!proofId) {
throw new Error('Missing required parameter: proofId');
}
const proof = proofLibrary.getProof(proofId);
if (!proof) {
throw new Error(`Proof not found: ${proofId}`);
}
let responseText = `Proof: ${proof.name}\n\n`;
responseText += `ID: ${proof.id}\n`;
responseText += `System: ${proof.system}\n`;
responseText += `Author: ${proof.author}\n`;
responseText += `Created: ${new Date(proof.createdAt).toLocaleString()}\n`;
responseText += `Usage Count: ${proof.usageCount}\n`;
responseText += `Success Rate: ${(proof.successRate * 100).toFixed(1)}%\n`;
if (proof.description) {
responseText += `\nDescription: ${proof.description}\n`;
}
if (proof.tags.length > 0) {
responseText += `Tags: ${proof.tags.join(', ')}\n`;
}
responseText += `\nPremises:\n`;
for (let i = 0; i < proof.premises.length; i++) {
responseText += `${i + 1}. ${proof.premises[i]}\n`;
}
responseText += `\nConclusion: ${proof.conclusion}\n`;
responseText += `\nProof Steps:\n`;
for (const step of proof.proofSteps) {
responseText += `${step.stepNumber}. ${step.statement}\n`;
responseText += ` ${step.justification}`;
if (step.rule) {
responseText += ` (${step.rule})`;
}
if (step.references && step.references.length > 0) {
responseText += ` [refs: ${step.references.join(', ')}]`;
}
responseText += `\n`;
}
if (proof.formalizedInput) {
responseText += `\nFormalized: ${proof.formalizedInput}\n`;
}
return {
content: [
{
type: "text",
text: responseText
}
],
isError: false
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Error retrieving proof';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Handle proof list tool call
*/
function handleProofListToolCall(args: any) {
try {
const { system, limit, offset } = args;
const proofs = proofLibrary.listProofs(system, limit || 50, offset || 0);
let responseText = `Proof Library\n\n`;
if (system) {
responseText += `System: ${system}\n`;
}
responseText += `Found: ${proofs.length} proof(s)\n\n`;
if (proofs.length === 0) {
responseText += `No proofs in the library.`;
} else {
for (let i = 0; i < proofs.length; i++) {
const proof = proofs[i];
responseText += `${i + 1}. ${proof.name}\n`;
responseText += ` ID: ${proof.id}\n`;
responseText += ` System: ${proof.system} | Author: ${proof.author}\n`;
responseText += ` Usage: ${proof.usageCount} | Success: ${(proof.successRate * 100).toFixed(1)}%\n`;
if (proof.tags.length > 0) {
responseText += ` Tags: ${proof.tags.join(', ')}\n`;
}
responseText += `\n`;
}
}
return {
content: [
{
type: "text",
text: responseText
}
],
isError: false
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Error listing proofs';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Handle proof stats tool call
*/
function handleProofStatsToolCall(args: any) {
try {
const stats = proofLibrary.getStats();
let responseText = `Proof Library Statistics\n\n`;
responseText += `Total Proofs: ${stats.totalProofs}\n`;
responseText += `Total Lemmas: ${stats.totalLemmas}\n`;
responseText += `Average Success Rate: ${(stats.averageSuccessRate * 100).toFixed(1)}%\n\n`;
responseText += `Proofs by System:\n`;
for (const [system, count] of Object.entries(stats.proofsBySystem)) {
responseText += ` ${system}: ${count}\n`;
}
responseText += `\nProofs by Author:\n`;
responseText += ` User: ${stats.proofsByAuthor.user}\n`;
responseText += ` Claude: ${stats.proofsByAuthor.claude}\n`;
if (stats.mostUsedProofs.length > 0) {
responseText += `\nMost Used Proofs:\n`;
for (let i = 0; i < Math.min(5, stats.mostUsedProofs.length); i++) {
const p = stats.mostUsedProofs[i];
responseText += ` ${i + 1}. ${p.name} (${p.usageCount} uses)\n`;
}
}
if (stats.recentProofs.length > 0) {
responseText += `\nRecent Proofs:\n`;
for (let i = 0; i < Math.min(5, stats.recentProofs.length); i++) {
const p = stats.recentProofs[i];
responseText += ` ${i + 1}. ${p.name} (${new Date(p.createdAt).toLocaleDateString()})\n`;
}
}
return {
content: [
{
type: "text",
text: responseText
}
],
isError: false
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Error retrieving statistics';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Handle assumption extraction tool call
*/
async function handleAssumptionExtractionToolCall(args: any) {
try {
const { premises, conclusion, system } = args;
if (!premises || !Array.isArray(premises)) {
throw new Error('Missing or invalid premises array');
}
if (!conclusion) {
throw new Error('Missing required parameter: conclusion');
}
const logicalSystem = system || 'propositional';
// Extract assumptions
const report = await assumptionExtractor.extractAssumptions(premises, conclusion, logicalSystem);
// Format results for MCP response
let responseText = `Assumption Analysis Report\n\n`;
responseText += `System: ${logicalSystem}\n`;
responseText += `Explicit Premises: ${report.explicitPremises.length}\n`;
responseText += `Hidden Assumptions: ${report.hiddenAssumptions.length}\n`;
responseText += `Validity Gaps: ${report.validityGaps.length}\n\n`;
// Explicit premises
if (report.explicitPremises.length > 0) {
responseText += `Explicit Premises:\n`;
for (let i = 0; i < report.explicitPremises.length; i++) {
responseText += ` ${i + 1}. ${report.explicitPremises[i]}\n`;
}
responseText += `\n`;
}
responseText += `Conclusion: ${conclusion}\n\n`;
// Hidden assumptions
if (report.hiddenAssumptions.length > 0) {
responseText += `Hidden Assumptions Detected:\n\n`;
for (let i = 0; i < report.hiddenAssumptions.length; i++) {
const a = report.hiddenAssumptions[i];
responseText += `${i + 1}. [${a.type.toUpperCase()}] ${a.statement}\n`;
responseText += ` Necessity: ${a.necessity}\n`;
responseText += ` Confidence: ${(a.confidence * 100).toFixed(0)}%\n`;
responseText += ` Explanation: ${a.explanation}\n`;
responseText += ` Source: ${a.source}\n\n`;
}
} else {
responseText += `No hidden assumptions detected.\n\n`;
}
// Validity gaps
if (report.validityGaps.length > 0) {
responseText += `Logical Validity Gaps:\n\n`;
for (let i = 0; i < report.validityGaps.length; i++) {
const gap = report.validityGaps[i];
responseText += `${i + 1}. ${gap.gapDescription}\n`;
if (gap.suggestedAssumptions.length > 0) {
responseText += ` Suggested: ${gap.suggestedAssumptions.join('; ')}\n`;
}
responseText += `\n`;
}
}
// Background knowledge
if (report.backgroundKnowledge.length > 0) {
responseText += `Background Knowledge Required:\n`;
for (const knowledge of report.backgroundKnowledge) {
responseText += ` • ${knowledge}\n`;
}
responseText += `\n`;
}
// Overall assessment
responseText += `Overall Assessment:\n`;
responseText += ` Argument Strength: ${report.overallAssessment.argumentStrength.toUpperCase()}\n`;
responseText += ` Total Assumptions: ${report.overallAssessment.assumptionCount}\n`;
responseText += ` Critical Gaps: ${report.overallAssessment.criticalGaps}\n\n`;
if (report.overallAssessment.recommendations.length > 0) {
responseText += `Recommendations:\n`;
for (const rec of report.overallAssessment.recommendations) {
responseText += ` • ${rec}\n`;
}
}
return {
content: [
{
type: "text",
text: responseText
}
],
isError: false
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Assumption extraction error';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Handle score operation for argument scoring
*/
async function handleScoreOperation(input: string, system: string, format: string) {
try {
// Parse input to extract premises and conclusion
// Expected format: "premise1. premise2. Therefore, conclusion"
const parts = input.split(/therefore[,\.]?\s+/i);
if (parts.length !== 2) {
throw new Error('Input must be in format: "premise1. premise2. Therefore, conclusion"');
}
const premisesText = parts[0].trim();
const conclusion = parts[1].trim();
// Split premises by period or semicolon
const premises = premisesText
.split(/[.;]\s+/)
.filter(p => p.trim().length > 0)
.map(p => p.trim());
if (premises.length === 0) {
throw new Error('No premises found');
}
// Determine the logical system
const logicalSystem = system === 'auto' ? 'propositional' : system;
// Score the argument
const score = await argumentScorer.scoreArgument(premises, conclusion, logicalSystem as any);
// Format response
let responseText = `Argument Score Report\n\n`;
responseText += `Overall Score: ${score.overallScore}/100 (Grade: ${score.grade})\n`;
responseText += `Comparison: ${score.comparisonToAverage}\n\n`;
responseText += `Component Scores:\n`;
for (const [name, component] of Object.entries(score.components)) {
responseText += `\n${name}:\n`;
responseText += ` Score: ${component.score}/100 (weight: ${(component.weight * 100).toFixed(0)}%)\n`;
responseText += ` ${component.explanation}\n`;
if (component.details && component.details.length > 0) {
for (const detail of component.details) {
responseText += ` • ${detail}\n`;
}
}
}
if (score.strengths.length > 0) {
responseText += `\nStrengths:\n`;
for (const strength of score.strengths) {
responseText += ` ✓ ${strength}\n`;
}
}
if (score.weaknesses.length > 0) {
responseText += `\nWeaknesses:\n`;
for (const weakness of score.weaknesses) {
responseText += ` ✗ ${weakness}\n`;
}
}
if (score.recommendations.length > 0) {
responseText += `\nRecommendations:\n`;
for (const rec of score.recommendations) {
responseText += ` → ${rec}\n`;
}
}
return {
content: [
{
type: "text",
text: responseText
}
],
isError: false
};
} catch (error) {
const errorMessage = error instanceof Error ? error.message : 'Scoring error';
return {
content: [
{
type: "text",
text: errorMessage
}
],
isError: true
};
}
}
/**
* Handle ping request
*/
function handlePing(params: any) {
return { status: "pong" };
}
// Handle process events
process.on('SIGINT', () => {
logger.info('SIGINT received, shutting down...');
process.exit(0);
});
process.on('uncaughtException', (error) => {
logger.error('Uncaught exception', {
error: error instanceof Error ? error.message : String(error),
stack: error instanceof Error ? error.stack : undefined
});
process.exit(1);
});
// Send server info on startup
logger.info('Logic Thinking MCP Server started');
logger.info('Awaiting JSON-RPC 2.0 requests...');
