hermes-brain/ideas/common-logic-iso-24707.org

Common Logic (ISO 24707) — Relevance to Passepartout

Common Logic (ISO/IEC 24707) is a framework for first-order logic languages designed for knowledge exchange. It defines an abstract syntax and model-theoretic semantics. Any concrete syntax (dialect) that maps to the abstract syntax inherits the semantics — and all CL dialects are automatically interoperable.

Three standard dialects: CLIF (Common Logic Interchange Format), CGIF (Conceptual Graph Interchange Format), XCL (XML-based). Additionally, RDF and OWL can be mapped to CL, making them interoperable with any CL dialect.

Relevance to Passepartout

The fact store interchange format. Passepartout's fact store uses plists internally — fast, native to Lisp, zero serialization cost. But between instances (Agora sync, backup/restore, export), a standardized format is needed. CLIF is a strong candidate because its first-order logic is a direct match for the gate rules ACL2 verifies. A CLIF-to-ACL2 translator is mechanically straightforward — both operate on first-order formulas.

The dialect architecture mirrors Passepartout. CL's defining insight: define abstract semantics, let any concrete syntax map to it, get interoperability for free. This is the exact same pattern as Passepartout's "one gate stack, many skills" — the gate stack defines the security ontology (abstract semantics), and skills (dialects) map their operations to it. CL's approach validates Passepartout's design choice and provides a theoretical framework for it.

ISO standard as a credential. For regulated industries, "the knowledge representation follows ISO/IEC 24707" is a strong signal. It says the format is not proprietary, has formal semantics, and has been reviewed by an international body. This matters for HIPAA, SOC2, FedRAMP, and any compliance framework that asks about data representation standards. It is a checkbox that enterprise procurement requires.

The RDF/OWL bridge. CL has defined translations to RDF and OWL. This means Passepartout can consume knowledge from the semantic web without building a separate RDF parser. The fact store stays in plists internally; CL is the serialization and interchange layer. Any enterprise knowledge graph expressed in OWL can be ingested as CLIF, translated to plists, and verified by ACL2.

Multiple implementations exist. There are CL reference implementations (some in Lisp) that can be adapted or used as guides rather than writing from scratch.

What Common Logic is NOT for Passepartout

Not a replacement for ACL2. CL is a knowledge representation standard, not a theorem prover. ACL2 proves theorems about gate rules. CLIF encodes the gate rules themselves. They are complementary: ACL2 verifies CLIF-encoded rule sets.

Not the internal representation. CLIF is verbose and not optimized for in-process use. The fact store should stay as plists internally. CL is the serialization layer — on the wire between Agora instances, in export files, in backup archives. This is the same pattern as JSON for web APIs: internal data structures are whatever is fastest, JSON is the interchange format.

Not a dialect to implement. Passepartout should not implement a full CLIF parser. The right approach is a thin translation layer: export plist → CLIF, import CLIF → ACL2-verified → plist. The AC Lisp ecosystem likely has CLIF libraries that can be wrapped.

The higher-order question

CL allows quantification over predicate and function symbols, which is technically a higher-order feature, despite being marketed as a first-order framework. This is directly relevant to Passepartout's roadmap: the system eventually wants a CIC prover for dependent types, and CL's approach — start from first-order, carefully extend with specific higher-order features — is the same strategy Passepartout uses with ACL2 + macro layers.

CL's treatment of higher-order features is instructive: it extends first-order semantics with specific mechanisms rather than adopting a full dependent type theory. The result is less expressive but more practical, easier to implement, and easier to verify. Passepartout's planned CIC prover should consider the same trade.

Verdict

Common Logic is relevant not as something to implement or replace, but as:

1. A natural serialization format for the fact store (Agora Notes, inter-instance sync)
2. An enterprise procurement checkbox (ISO standard)
3. A theoretical validation of Passepartout's dialect-based architecture
4. A bridge to RDF/OWL data sources
5. A cautionary example for the CIC prover design (careful about higher-order scope)

The right time to integrate it: when Agora Notes need a standard knowledge interchange format for inter-instance communication. Before that, it is a reference worth reading but not implementing. The CL approach informs the sufficiency flip strategy and the cost structure of encoding domain knowledge.