47 lines
5.1 KiB
Org Mode
47 lines
5.1 KiB
Org Mode
:PROPERTIES:
|
|
:ID: 04c2f221-c54f-51e5-b40a-48822cd16d45
|
|
:END:
|
|
#+title: Common Logic (ISO 24707) — Relevance to Passepartout
|
|
#+filetags: :passepartout:knowledge:logic:standards:iso:
|
|
|
|
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 ([[file:agora.org][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 [[file:gate-rule-encoding.org][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 [[file:compliance/hipaa.org][HIPAA]], SOC2, [[file:compliance/fedramp.org][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 [[file:sufficiency-flip.org][sufficiency flip]] strategy and the [[file:cost-structure.org][cost structure]] of encoding domain knowledge.
|