semantic-explanation-targets
repository URL pending
Scope
semantic-explanation-targets is an integration library for attaching structured semantic explanations to logic, ontology, and digital-hardware examples. Its direct target modules exercise OWL class subsumption and Spartan clock-domain claims through both direct and compact explanation forms. The Industry hierarchy develops domain specifications for batch-reactor control, aircraft maintenance, and redundant motor-permit safety circuits. Discourse profiles extend that coverage to named industrial scenarios including rail movement, medicine recalls, cold chains, pump starts, burner ignition, and wind energization. Candidate-run and showcase modules collect the target readings and evidence variants into a common set of worked integrations.
Most important results
The OWL target records reflexive and transitive subclass explanations in both direct and compact textual forms. The Spartan target connects clock-domain soundness, register-update behavior, and safety-preserving motor-control traces to generated explanations. The industry formalizations include proved discharge interlocks for batch reactors, maintenance-record conditions for return-to-service release, and redundancy preservation across audited control sequences. The candidate suite exposes canonical, compact, structured, domain, and evidence readings for multiple case studies, allowing the same explanation machinery to be compared across targets.
Library modules
13 checked modules
Select a module to inspect its generated Agda source view.