import Database from 'better-sqlite3';
import { v4 as uuidv4 } from 'uuid';
import { LogicalSystem } from './types.js';
import { Loggers } from './utils/logger.js';
import * as path from 'path';
import * as fs from 'fs';
const logger = Loggers.server;
/**
* Represents a single step in a logical proof
*/
export interface ProofStep {
stepNumber: number;
statement: string;
justification: string;
rule?: string;
references?: number[]; // References to previous steps
}
/**
* Represents a saved proof in the library
*/
export interface SavedProof {
id: string;
name: string;
description?: string;
system: LogicalSystem;
premises: string[];
conclusion: string;
proofSteps: ProofStep[];
formalizedInput?: string;
createdAt: number;
updatedAt: number;
usageCount: number;
successRate: number;
author: 'user' | 'claude';
tags: string[];
}
/**
* Represents a reusable lemma (sub-proof)
*/
export interface Lemma {
id: string;
name: string;
description?: string;
system: LogicalSystem;
premises: string[];
conclusion: string;
proofId?: string; // Reference to full proof if applicable
usageCount: number;
tags: string[];
}
/**
* Search options for finding proofs
*/
export interface ProofSearchOptions {
query?: string; // Full-text search query
system?: LogicalSystem;
tags?: string[];
author?: 'user' | 'claude';
minSuccessRate?: number;
limit?: number;
offset?: number;
sortBy?: 'relevance' | 'usage' | 'date' | 'success_rate';
sortOrder?: 'asc' | 'desc';
}
/**
* Statistics about the proof library
*/
export interface ProofLibraryStats {
totalProofs: number;
totalLemmas: number;
proofsBySystem: Record<LogicalSystem, number>;
mostUsedProofs: Array<{ id: string; name: string; usageCount: number }>;
averageSuccessRate: number;
proofsByAuthor: { user: number; claude: number };
recentProofs: Array<{ id: string; name: string; createdAt: number }>;
}
/**
* Result of composing lemmas into a proof
*/
export interface CompositionResult {
success: boolean;
composedProof?: SavedProof;
steps: ProofStep[];
message: string;
warnings?: string[];
}
/**
* Proof Library for storing, searching, and reusing logical proofs
*/
export class ProofLibrary {
private db: Database.Database;
private dbPath: string;
constructor(dbPath: string = './data/proofs.db') {
// Resolve to absolute path to avoid issues with relative paths
this.dbPath = path.resolve(dbPath);
// Ensure data directory exists
const dir = path.dirname(this.dbPath);
if (!fs.existsSync(dir)) {
fs.mkdirSync(dir, { recursive: true });
}
this.db = new Database(this.dbPath);
this.initializeDatabase();
logger.info(`ProofLibrary initialized at ${this.dbPath}`);
}
/**
* Initialize database schema
*/
private initializeDatabase(): void {
this.db.exec(`
CREATE TABLE IF NOT EXISTS proofs (
id TEXT PRIMARY KEY,
name TEXT NOT NULL,
description TEXT,
system TEXT NOT NULL,
premises TEXT NOT NULL,
conclusion TEXT NOT NULL,
proof_steps TEXT NOT NULL,
formalized_input TEXT,
created_at INTEGER NOT NULL,
updated_at INTEGER NOT NULL,
usage_count INTEGER DEFAULT 0,
success_rate REAL DEFAULT 1.0,
author TEXT DEFAULT 'user'
);
CREATE TABLE IF NOT EXISTS proof_tags (
proof_id TEXT NOT NULL,
tag TEXT NOT NULL,
PRIMARY KEY (proof_id, tag),
FOREIGN KEY (proof_id) REFERENCES proofs(id) ON DELETE CASCADE
);
CREATE TABLE IF NOT EXISTS lemmas (
id TEXT PRIMARY KEY,
name TEXT NOT NULL,
description TEXT,
system TEXT NOT NULL,
premises TEXT NOT NULL,
conclusion TEXT NOT NULL,
proof_id TEXT,
usage_count INTEGER DEFAULT 0,
FOREIGN KEY (proof_id) REFERENCES proofs(id) ON DELETE SET NULL
);
CREATE TABLE IF NOT EXISTS lemma_tags (
lemma_id TEXT NOT NULL,
tag TEXT NOT NULL,
PRIMARY KEY (lemma_id, tag),
FOREIGN KEY (lemma_id) REFERENCES lemmas(id) ON DELETE CASCADE
);
CREATE VIRTUAL TABLE IF NOT EXISTS proof_search USING fts5(
proof_id UNINDEXED,
name,
description,
premises,
conclusion,
tags
);
CREATE INDEX IF NOT EXISTS idx_proofs_system ON proofs(system);
CREATE INDEX IF NOT EXISTS idx_proofs_author ON proofs(author);
CREATE INDEX IF NOT EXISTS idx_proofs_created_at ON proofs(created_at);
CREATE INDEX IF NOT EXISTS idx_proofs_usage_count ON proofs(usage_count);
CREATE INDEX IF NOT EXISTS idx_proofs_success_rate ON proofs(success_rate);
`);
logger.info('Database schema initialized');
}
/**
* Save a proof to the library
*/
saveProof(
name: string,
description: string | undefined,
system: LogicalSystem,
premises: string[],
conclusion: string,
proofSteps: ProofStep[],
tags: string[] = [],
author: 'user' | 'claude' = 'user',
formalizedInput?: string
): SavedProof {
const id = uuidv4();
const now = Date.now();
const proof: SavedProof = {
id,
name,
description,
system,
premises,
conclusion,
proofSteps,
formalizedInput,
createdAt: now,
updatedAt: now,
usageCount: 0,
successRate: 1.0,
author,
tags
};
const insertProof = this.db.prepare(`
INSERT INTO proofs (
id, name, description, system, premises, conclusion, proof_steps,
formalized_input, created_at, updated_at, usage_count, success_rate, author
) VALUES (?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?)
`);
insertProof.run(
id,
name,
description || null,
system,
JSON.stringify(premises),
conclusion,
JSON.stringify(proofSteps),
formalizedInput || null,
now,
now,
0,
1.0,
author
);
// Insert tags (use INSERT OR IGNORE to handle duplicates)
if (tags.length > 0) {
const insertTag = this.db.prepare('INSERT OR IGNORE INTO proof_tags (proof_id, tag) VALUES (?, ?)');
for (const tag of tags) {
insertTag.run(id, tag);
}
}
// Insert into FTS table
const insertFTS = this.db.prepare(`
INSERT INTO proof_search (proof_id, name, description, premises, conclusion, tags)
VALUES (?, ?, ?, ?, ?, ?)
`);
insertFTS.run(
id,
name,
description || '',
premises.join(' '),
conclusion,
tags.join(' ')
);
logger.info(`Saved proof: ${name} (${id})`);
return proof;
}
/**
* Get a proof by ID
*/
getProof(id: string): SavedProof | null {
const row = this.db
.prepare('SELECT * FROM proofs WHERE id = ?')
.get(id) as any;
if (!row) {
return null;
}
// Get tags
const tags = this.db
.prepare('SELECT tag FROM proof_tags WHERE proof_id = ?')
.all(id)
.map((r: any) => r.tag);
return this.rowToProof(row, tags);
}
/**
* Search for proofs
*/
searchProofs(options: ProofSearchOptions = {}): SavedProof[] {
const {
query,
system,
tags,
author,
minSuccessRate,
limit = 20,
offset = 0,
sortBy = 'relevance',
sortOrder = 'desc'
} = options;
let sql: string;
let params: any[] = [];
try {
if (query) {
// Full-text search - sanitize query to handle special characters
const safeQuery = query.replace(/['"]/g, '');
// If query is empty after sanitization, return empty results
if (!safeQuery.trim()) {
logger.warn('Empty search query after sanitization');
return [];
}
sql = `
SELECT p.*, GROUP_CONCAT(pt.tag) as tags
FROM proofs p
INNER JOIN proof_search ps ON p.id = ps.proof_id
LEFT JOIN proof_tags pt ON p.id = pt.proof_id
WHERE ps.proof_search MATCH ?
`;
params.push(safeQuery);
} else {
// Regular search
sql = `
SELECT p.*, GROUP_CONCAT(pt.tag) as tags
FROM proofs p
LEFT JOIN proof_tags pt ON p.id = pt.proof_id
WHERE 1=1
`;
}
// Add filters
if (system && system !== 'auto') {
sql += ' AND p.system = ?';
params.push(system);
}
if (author) {
sql += ' AND p.author = ?';
params.push(author);
}
if (minSuccessRate !== undefined) {
sql += ' AND p.success_rate >= ?';
params.push(minSuccessRate);
}
if (tags && tags.length > 0) {
sql += ` AND p.id IN (
SELECT proof_id FROM proof_tags WHERE tag IN (${tags.map(() => '?').join(',')})
GROUP BY proof_id HAVING COUNT(*) = ?
)`;
params.push(...tags, tags.length);
}
// Add grouping
sql += ' GROUP BY p.id';
// Add sorting
const sortColumn = {
relevance: query ? 'rank' : 'p.created_at',
usage: 'p.usage_count',
date: 'p.created_at',
success_rate: 'p.success_rate'
}[sortBy];
sql += ` ORDER BY ${sortColumn} ${sortOrder.toUpperCase()}`;
// Add pagination
sql += ' LIMIT ? OFFSET ?';
params.push(limit, offset);
const rows = this.db.prepare(sql).all(...params) as any[];
return rows.map(row => {
const tags = row.tags ? row.tags.split(',') : [];
return this.rowToProof(row, tags);
});
} catch (error) {
// Log the error for debugging
logger.error(`Database search error: ${error instanceof Error ? error.message : String(error)}`);
// Return empty array instead of throwing - graceful degradation
// This handles cases like searching for non-existent terms in FTS5
return [];
}
}
/**
* List all proofs with optional filtering
*/
listProofs(system?: LogicalSystem, limit: number = 50, offset: number = 0): SavedProof[] {
let sql = `
SELECT p.*, GROUP_CONCAT(pt.tag) as tags
FROM proofs p
LEFT JOIN proof_tags pt ON p.id = pt.proof_id
`;
const params: any[] = [];
if (system && system !== 'auto') {
sql += ' WHERE p.system = ?';
params.push(system);
}
sql += ' GROUP BY p.id ORDER BY p.created_at DESC LIMIT ? OFFSET ?';
params.push(limit, offset);
const rows = this.db.prepare(sql).all(...params) as any[];
return rows.map(row => {
const tags = row.tags ? row.tags.split(',') : [];
return this.rowToProof(row, tags);
});
}
/**
* Update proof usage statistics
*/
recordUsage(proofId: string, success: boolean): void {
const proof = this.getProof(proofId);
if (!proof) {
throw new Error(`Proof not found: ${proofId}`);
}
const newUsageCount = proof.usageCount + 1;
// Calculate new success rate using exponential moving average
const alpha = 0.2; // Weight for new observation
const newSuccessRate = proof.successRate * (1 - alpha) + (success ? 1 : 0) * alpha;
this.db
.prepare('UPDATE proofs SET usage_count = ?, success_rate = ?, updated_at = ? WHERE id = ?')
.run(newUsageCount, newSuccessRate, Date.now(), proofId);
logger.info(`Updated usage for proof ${proofId}: count=${newUsageCount}, rate=${newSuccessRate.toFixed(2)}`);
}
/**
* Delete a proof
*/
deleteProof(proofId: string): boolean {
const result = this.db.prepare('DELETE FROM proofs WHERE id = ?').run(proofId);
if (result.changes > 0) {
// Delete from FTS table
this.db.prepare('DELETE FROM proof_search WHERE proof_id = ?').run(proofId);
logger.info(`Deleted proof: ${proofId}`);
return true;
}
return false;
}
/**
* Save a lemma (reusable sub-proof)
*/
saveLemma(
name: string,
description: string | undefined,
system: LogicalSystem,
premises: string[],
conclusion: string,
tags: string[] = [],
proofId?: string
): Lemma {
const id = uuidv4();
const lemma: Lemma = {
id,
name,
description,
system,
premises,
conclusion,
proofId,
usageCount: 0,
tags
};
const insertLemma = this.db.prepare(`
INSERT INTO lemmas (id, name, description, system, premises, conclusion, proof_id, usage_count)
VALUES (?, ?, ?, ?, ?, ?, ?, ?)
`);
insertLemma.run(
id,
name,
description || null,
system,
JSON.stringify(premises),
conclusion,
proofId || null,
0
);
// Insert tags
if (tags.length > 0) {
const insertTag = this.db.prepare('INSERT INTO lemma_tags (lemma_id, tag) VALUES (?, ?)');
for (const tag of tags) {
insertTag.run(id, tag);
}
}
logger.info(`Saved lemma: ${name} (${id})`);
return lemma;
}
/**
* Get a lemma by ID
*/
getLemma(id: string): Lemma | null {
const row = this.db
.prepare('SELECT * FROM lemmas WHERE id = ?')
.get(id) as any;
if (!row) {
return null;
}
// Get tags
const tags = this.db
.prepare('SELECT tag FROM lemma_tags WHERE lemma_id = ?')
.all(id)
.map((r: any) => r.tag);
return this.rowToLemma(row, tags);
}
/**
* Search for lemmas
*/
searchLemmas(system?: LogicalSystem, tags?: string[]): Lemma[] {
let sql = 'SELECT l.*, GROUP_CONCAT(lt.tag) as tags FROM lemmas l LEFT JOIN lemma_tags lt ON l.id = lt.lemma_id';
const params: any[] = [];
const conditions: string[] = [];
if (system && system !== 'auto') {
conditions.push('l.system = ?');
params.push(system);
}
if (tags && tags.length > 0) {
conditions.push(`l.id IN (
SELECT lemma_id FROM lemma_tags WHERE tag IN (${tags.map(() => '?').join(',')})
GROUP BY lemma_id HAVING COUNT(*) = ?
)`);
params.push(...tags, tags.length);
}
if (conditions.length > 0) {
sql += ' WHERE ' + conditions.join(' AND ');
}
sql += ' GROUP BY l.id ORDER BY l.usage_count DESC';
const rows = this.db.prepare(sql).all(...params) as any[];
return rows.map(row => {
const tags = row.tags ? row.tags.split(',') : [];
return this.rowToLemma(row, tags);
});
}
/**
* Compose lemmas into a larger proof
*/
composeLemmas(
name: string,
lemmaIds: string[],
bridgingSteps: ProofStep[] = [],
description?: string,
tags: string[] = []
): CompositionResult {
const lemmas: Lemma[] = [];
// Fetch all lemmas
for (const id of lemmaIds) {
const lemma = this.getLemma(id);
if (!lemma) {
return {
success: false,
steps: [],
message: `Lemma not found: ${id}`
};
}
lemmas.push(lemma);
}
// Check that all lemmas use compatible systems
const systems = new Set(lemmas.map(l => l.system));
if (systems.size > 1) {
return {
success: false,
steps: [],
message: `Cannot compose lemmas from different logical systems: ${Array.from(systems).join(', ')}`,
warnings: ['Consider using logic translation to convert lemmas to a common system']
};
}
const system = lemmas[0].system;
// Compose proof steps
const composedSteps: ProofStep[] = [];
let stepNumber = 1;
// Add lemma applications
for (const lemma of lemmas) {
// Add premises
for (const premise of lemma.premises) {
composedSteps.push({
stepNumber: stepNumber++,
statement: premise,
justification: `Premise from lemma: ${lemma.name}`
});
}
// Add conclusion
composedSteps.push({
stepNumber: stepNumber++,
statement: lemma.conclusion,
justification: `Application of lemma: ${lemma.name}`,
rule: 'Lemma Application',
references: Array.from({ length: lemma.premises.length }, (_, i) => stepNumber - lemma.premises.length - 1 + i)
});
// Update lemma usage
this.db.prepare('UPDATE lemmas SET usage_count = usage_count + 1 WHERE id = ?').run(lemma.id);
}
// Add bridging steps
for (const step of bridgingSteps) {
composedSteps.push({
...step,
stepNumber: stepNumber++
});
}
// Collect all premises and determine final conclusion
const allPremises = lemmas.flatMap(l => l.premises);
const finalConclusion = bridgingSteps.length > 0
? bridgingSteps[bridgingSteps.length - 1].statement
: lemmas[lemmas.length - 1].conclusion;
// Save the composed proof
const composedProof = this.saveProof(
name,
description || `Composed from lemmas: ${lemmas.map(l => l.name).join(', ')}`,
system,
allPremises,
finalConclusion,
composedSteps,
[...tags, 'composed'],
'claude'
);
return {
success: true,
composedProof,
steps: composedSteps,
message: `Successfully composed ${lemmas.length} lemmas into proof: ${name}`
};
}
/**
* Get statistics about the proof library
*/
getStats(): ProofLibraryStats {
const totalProofs = (this.db.prepare('SELECT COUNT(*) as count FROM proofs').get() as any).count;
const totalLemmas = (this.db.prepare('SELECT COUNT(*) as count FROM lemmas').get() as any).count;
// Proofs by system
const systemRows = this.db.prepare('SELECT system, COUNT(*) as count FROM proofs GROUP BY system').all() as any[];
const proofsBySystem = systemRows.reduce((acc, row) => {
acc[row.system as LogicalSystem] = row.count;
return acc;
}, {} as Record<LogicalSystem, number>);
// Most used proofs
const mostUsedRows = this.db
.prepare('SELECT id, name, usage_count FROM proofs ORDER BY usage_count DESC LIMIT 10')
.all() as any[];
const mostUsedProofs = mostUsedRows.map(p => ({
id: p.id,
name: p.name,
usageCount: p.usage_count
}));
// Average success rate
const avgRow = this.db.prepare('SELECT AVG(success_rate) as avg FROM proofs').get() as any;
const averageSuccessRate = avgRow.avg || 0;
// Proofs by author
const authorRows = this.db.prepare('SELECT author, COUNT(*) as count FROM proofs GROUP BY author').all() as any[];
const proofsByAuthor = authorRows.reduce((acc, row) => {
acc[row.author as 'user' | 'claude'] = row.count;
return acc;
}, { user: 0, claude: 0 });
// Recent proofs
const recentProofs = this.db
.prepare('SELECT id, name, created_at FROM proofs ORDER BY created_at DESC LIMIT 10')
.all() as any[];
return {
totalProofs,
totalLemmas,
proofsBySystem,
mostUsedProofs,
averageSuccessRate,
proofsByAuthor,
recentProofs: recentProofs.map(p => ({ id: p.id, name: p.name, createdAt: p.created_at }))
};
}
/**
* Convert database row to SavedProof object
*/
private rowToProof(row: any, tags: string[]): SavedProof {
return {
id: row.id,
name: row.name,
description: row.description,
system: row.system as LogicalSystem,
premises: JSON.parse(row.premises),
conclusion: row.conclusion,
proofSteps: JSON.parse(row.proof_steps),
formalizedInput: row.formalized_input,
createdAt: row.created_at,
updatedAt: row.updated_at,
usageCount: row.usage_count,
successRate: row.success_rate,
author: row.author as 'user' | 'claude',
tags
};
}
/**
* Convert database row to Lemma object
*/
private rowToLemma(row: any, tags: string[]): Lemma {
return {
id: row.id,
name: row.name,
description: row.description,
system: row.system as LogicalSystem,
premises: JSON.parse(row.premises),
conclusion: row.conclusion,
proofId: row.proof_id,
usageCount: row.usage_count,
tags
};
}
/**
* Close the database connection
*/
close(): void {
this.db.close();
logger.info('ProofLibrary database connection closed');
}
}
