| 1. Domain | 1.1 Scope of the Domain | Boundaries | The range of phenomena the science includes and excludes. | Studies algorithmic and human–machine systems for deriving proofs, solving logical problems, and constructing formal reasoning artifacts. Includes automated theorem proving, SAT/SMT solving, proof assistants, interactive proof construction, program verification, and reasoning engines. Excludes purely philosophical epistemic reasoning except when formalized. |
| | Scale | The spatial, temporal, or organizational level at which the science operates (e.g., quantum, cellular, social, cosmic). | Operates at computational, symbolic, and interactive scales: algorithmic proof search, term-rewriting scales, tactic-level reasoning, solver decision procedures, human-guided formal derivations, and large-scale verification projects spanning thousands of proof steps. |
| 1.2 Ontological Commitments | Entities | The kinds of things assumed to exist within the domain (particles, organisms, agents, fields, etc.). | Logical formulas, terms, proof objects, solver states, heuristics, decision procedures, search trees, tactic scripts, interactive proof states, constraint sets, models and countermodels, rewrite rules, unification artifacts. |
| | Properties | The fundamental attributes these entities possess (mass, charge, genotype, preference, etc.). | Satisfiability, validity, proof completeness, solver soundness, search depth, heuristic strength, tactic correctness, termination, convergence of search, model consistency, constraint propagation behavior. |
| | Categories | The basic ontological types used to classify domain elements (substances, processes, relations, structures). | Automated theorem provers, SMT solvers, SAT solvers, interactive proof assistants (Coq, Lean, Isabelle, HOL Light), decision procedures, rewriting systems, type-theoretic reasoning engines, hybrid automated–interactive systems. |
| 1.3 State-Variables | Variables | The measurable or definable properties that describe system conditions. | Current solver configuration, active constraints, search frontier, clause or formula sets, tactic stack, goal state, rewrite state, unification constraints, partial models, partial proofs, proof obligations. |
| | Parameterization | How variables encode and represent the system’s state. | Encoded via solver heuristics, search-depth bounds, rewrite rules, unification modes, tactic parameters, model bounds, constraint propagation strategies, decision-procedure parameters, and resource ceilings (time, memory). |
| 1.4 Admissible Idealizations | Simplifications | Conceptual reductions used to make the domain tractable (point masses, rational agents, perfect gases). | Idealized heuristics, abstracted search structures, simplified constraint languages, canonical normal forms, abstraction of human input into tactics, reduction of rich type systems into core calculi, simplified encodings for automated solving. |
| | Validity Conditions | The limits and contexts in which idealizations hold or break down. | Break down when heuristics fail on adversarial inputs, when constraint languages require expressiveness beyond solver support, when interactive proofs rely on noncanonical tactics, or when abstractions hide crucial structural information. |
| 1.5 Domain Assumptions | Structural Assumptions | Background ontological stances such as determinism, continuity, randomness, discreteness. | Reasoning is algorithmically representable; solvers are sound and (ideally) complete; tactics preserve correctness; proof objects are verifiable; constraint propagation is monotonic; interactions fit within formal proof frameworks. |
| | Implicit Commitments | Unstated but necessary assumptions that shape the field’s conceptual structure. | Assumes trust in core kernels of proof assistants, solver correctness, stability of heuristics, faithful translation of user intentions in interactive systems, and reliable grounding of complex reasoning into formal calculi. |
| 1.6 Internal Coherence Requirements | Consistency | The demand that domain concepts do not contradict one another. | Solver rules must not contradict one another; tactic-driven transformations must maintain proof validity; search procedures must align with foundational logic; proof objects must pass independent kernel verification. |
| | Compatibility | The requirement that entities, variables, and assumptions fit together into a unified descriptive framework. | Requires alignment between automated engines and foundational proof kernels, harmony across decision procedures, coherence of interactive tactics with core logical rules, and integrated consistency among solver modules and proof frameworks. |
| 2. Evidence Layer | 2.1 Observable Phenomena | Observables | The aspects of the domain that can produce detectable signals accessible to measurement. | Solver decisions, branching behavior, search-tree growth, tactic execution traces, proof-state transitions, model generation, constraint propagation steps, unification attempts, backtracking behavior, time-to-solve, failure modes. |
| | Detection Limits | The boundaries of what can be resolved or sensed by current instruments or methods. | Bounded by computational complexity of underlying logic (NP, PSPACE, EXPTIME), incomplete heuristics, inability to detect deep contradictions, limited model searches, timeout constraints, tactic incompleteness, and inability to explore infinite or extremely large search spaces. |
| 2.2 Measurement Systems | Units | Standardized quantifications (meters, seconds, volts, decibels, dollars, etc.) necessary for consistent comparison. | Time (ms/s), memory usage, number of solver steps, proof length, search depth, number of tactics executed, number of constraints generated, model size, backtracking count, branching factor, number of rewrite operations. |
| | Instruments | Devices and tools (microscopes, spectrometers, sensors, surveys, detectors) used to produce measurements. | SAT/SMT solvers, theorem provers (Vampire, E Prover), interactive proof assistants (Coq, Lean, Isabelle, HOL4), model checkers, constraint solvers, unification engines, rewriting systems, tactic profilers, solver logging frameworks. |
| 2.3 Operational Definitions | Definitions | Terms defined by specific measurement procedures, ensuring empirical clarity. | Proof success defined via kernel verification; solver success defined via satisfiable/unsatisfiable output; model validity defined via constraint satisfaction; tactic correctness defined by kernel acceptance; search node defined via solver decision state. |
| | Procedures | The explicit steps required to perform a measurement in a reproducible way. | Running automated proof search, executing tactic sequences, building interactive proofs step-by-step, applying rewrite rules, generating models/countermodels, measuring runtime and memory, profiling solver heuristics, extracting proof objects. |
| 2.4 Data Acquisition | Protocols | Formal processes for gathering data under controlled or standardized conditions. | Standardized benchmarking on logical theories, controlled solver configurations, uniform tactic scripts for reproducibility, systematic model-checking runs, replayable interactive proof sessions, fixed test suites for decision procedures. |
| | Sampling | Rules determining which subset of the domain is measured and how representative it is. | Selecting representative logical problems (SAT benchmarks, SMT-LIB suites), sampling interactive proofs across domains (algebra, analysis, type theory), testing solver heuristics on random or adversarial formulas, model sampling under varied constraints. |
| 2.5 Data Character & Format | Data Types | The form raw evidence takes (time series, spectra, images, counts, qualitative records). | Solver logs, proof objects, tactic-trace files, model and countermodel data, constraint sets, search trees, rewrite traces, unification graphs, timed performance traces, execution summaries. |
| | Resolution | The granularity or precision with which data is captured. | Determined by granularity of solver logs, precision of timing measurements, detail of tactic traces, model fidelity, completeness of search-tree capture, and the expressiveness of recorded proof objects. |
| 2.6 Reliability & Calibration | Calibration | Adjustment procedures ensuring instruments produce accurate results. | Validating solver outputs via independent checkers, verifying proof objects with trusted kernels, comparing solver decisions under identical conditions, calibrating heuristics, ensuring stable tactic behavior across versions, and cross-checking model generation. |
| | Error Characterization | Identification and quantification of noise, uncertainty, bias, and measurement error. | Solver misfires, incompleteness failures, tactic misapplication, kernel rejections, unification failures, rewrite-loop errors, inconsistent model generation, timeouts, nondeterministic solver variance, and incorrect logging outputs. |
| 3. Structural Layer | 3.1 Patterns & Regularities | Laws / Relations | Stable, repeatable patterns governing how observables behave across conditions. | Solver branching laws, constraint propagation patterns, rewrite-system confluence behavior, search-tree monotonicity, model construction regularities, tactic–search interactions, completeness/soundness relations, SAT/SMT decision patterns, proof normalization behaviors. |
| | Invariants | Quantities or properties that remain constant under transformations (symmetries, conservation laws). | Kernel-verification invariance, soundness invariants of solver rules, confluence invariants in rewrite systems, preservation of logical equivalence under tactics, structural invariants in search trees, termination guarantees of decision procedures. |
| 3.2 Causal Architecture | Mechanisms | Underlying processes or structures that produce the observed regularities. | Clause learning, unit propagation, DPLL branching, congruence closure, unification, rewriting, tactic execution, model construction, constraint propagation, heuristic-driven pruning, kernel checking as final cause of correctness. |
| | Pathways | Organized sequences of interactions forming a causal chain or network. | Solver decision → propagation → conflict → backjump → learned clause; interactive reasoning pathway: goal → tactic sequence → proof object → kernel verification; SMT path: theory propagation → model candidate → consistency check; rewriting path: term → rewrite chain → normal form. |
| 3.3 Theoretical Vocabulary | Concepts | Core terms that encode the domain’s structure (force, gene, equilibrium, field). | Search space, heuristic, proof object, tactic, kernel, model, countermodel, constraint, congruence closure, DPLL, CDCL, unification, rewriting, decision procedure, satisfiability, validity, termination, completeness. |
| | Classifications | Taxonomies, categories, or typologies that organize entities and relations. | Automated vs. interactive reasoning, SAT vs. SMT solvers, first-order vs. higher-order provers, sequent-based vs. rewriting-based systems, kernel-based proof assistants, DPLL/CDCL solvers, Euler-style vs. tactic-style proofs, symbolic vs. model-based reasoning systems. |
| 3.4 Formal Representations | Equations | Mathematical constructs expressing laws, relations, or mechanisms. | Unification equations, rewrite rules, constraint equations, congruence relations, Boolean propagation equations, SMT theory axioms, rewriting-system reduction equations, term-rewriting or search-cost recurrence relations. |
| | Models | Structured representations—mathematical, computational, or conceptual—used to predict and explain phenomena. | Proof trees, search trees, DAG derivations, model graphs, unification graphs, rewrite graphs, constraint graphs, tactic-execution trees, SAT/SMT solver state-transition models, kernel-verification models. |
| 3.5 Idealized Structures | Simplified Models | Purposeful abstractions that capture essential dynamics while omitting irrelevant detail. | Idealized DPLL/CDCL solvers, simplified rewrite systems, canonical constraint languages, reduced tactic libraries, abstract search models, minimal core kernels, simplified unification algorithms, symbolic model constructions. |
| | Limit Conditions | Regimes where specific models or approximations hold (classical vs. quantum, linear vs. nonlinear). | Failures under undecidable logics, infinite search spaces, heuristics that break on adversarial instances, nonterminating rewrite systems, tactics that do not normalize, model search exploding combinatorially, and solver incompleteness for higher-order theories. |
| 3.6 Integrative Frameworks | Unifying Theories | Higher-order structures that connect disparate laws or mechanisms under a coherent whole. | Curry–Howard (proofs-as-programs) link to interactive systems, SAT/SMT as unifying engines for first-order reasoning, rewriting logic as a meta-framework, congruence-closure and decision-procedure integration frameworks, kernel-verification as the final unifying correctness mechanism. |
| | Interdisciplinary Links | Points where the theory connects to adjacent sciences or larger explanatory systems. | Links to programming languages (type theory, compiler verification), artificial intelligence (search heuristics, planning), formal methods (verification, model checking), complexity theory, logic programming, automated deduction, and software engineering. |
| 4. Method Layer | 4.1 Inquiry Design | Experimental Design | Structured plans for manipulating variables to test causal claims. | Manipulating solver heuristics, changing branching strategies, adjusting rewrite rules, altering tactic sequences, modifying constraint languages, controlling resource limits (time/memory), toggling theory solvers in SMT, and enabling/disabling model-building modes to test reasoning performance. |
| | Observational Design | Systematic approaches for gathering non-manipulated data (surveys, field studies, natural experiments). | Observing solver behavior without intervention: tracking search depth, clause propagation, rewrite convergence, model generation, tactic performance, kernel-verification times, and heuristic-driven changes in reasoning trajectories. |
| 4.2 Testing & Validation | Hypothesis Testing | Procedures for evaluating whether evidence supports or contradicts specific claims. | Testing whether a solver is complete for a fragment, checking soundness of new decision procedures, verifying tactic correctness via kernel acceptance, validating model generation, assessing rewrite-system confluence, and testing new heuristics across standardized benchmarks. |
| | Replication | The requirement that results be independently reproducible under similar conditions. | Re-running solver benchmarks with identical parameters, repeating interactive proof sessions via script replay, verifying proof objects with independent kernels, replicating model-checking results, and comparing solver logs across implementations and versions. |
| 4.3 Inference & Evaluation | Statistical Inference | Rules for drawing conclusions from noisy or incomplete data. | Analyzing time and memory distributions across benchmarks, evaluating heuristic effectiveness, comparing proof lengths under different tactics, estimating failure rates, assessing model-generation reliability, and quantifying search-tree growth patterns. |
| | Model Comparison | Criteria (fit, simplicity, predictive accuracy, robustness) used to evaluate competing models. | Comparing SAT vs. SMT vs. first-order solvers, comparing proof assistants by kernel strength and expressiveness, evaluating differences between tactic-driven proofs and automated proofs, comparing rewrite vs. decision-procedure reasoning, and benchmarking solver performance across problem classes. |
| 4.4 Error Management | Error Analysis | Identification and quantification of random and systematic errors. | Identifying incorrect solver decisions, tactic misapplications, kernel rejections, unification failures, rewrite loops, constraint propagation errors, model-inconsistency errors, nondeterministic solver outcomes, and logging or instrumentation failures. |
| | Bias Control | Methods for minimizing subjective, instrumental, or procedural biases. | Avoiding solver-configuration bias, using standardized benchmark suites, preventing cherry-picked examples, neutralizing tactic-order effects, controlling for hardware variance, and ensuring fairness across solver comparisons. |
| 4.5 Adjudication & Revision | Peer Scrutiny | Collective evaluation of claims through critique, review, and debate. | Reviewing solver algorithms, auditing kernel correctness, evaluating tactic definitions, comparing independent implementations of decision procedures, replicating experimental results, performing formal correctness proofs of reasoning components, and community-driven evaluation via competition benchmarks. |
| | Theory Revision | Procedures for modifying, replacing, or discarding models based on new evidence. | Updating solver heuristics, refining rewrite rules, extending decision procedures, repairing tactic libraries, modifying kernel foundations if needed, integrating new theories, improving proof-search algorithms, and recalibrating solvers based on benchmark results. |
| 4.6 Integrity Conditions | Transparency | Requirements to disclose methods, data, assumptions, and limitations. | Full disclosure of solver configurations, tactic scripts, kernel rules, rewrite systems, model-checker parameters, benchmark datasets, and detailed proof objects; documenting assumptions and limitations of reasoning engines. |
| | Ethical Standards | Norms ensuring responsible conduct in experimentation, data handling, and publication. | Ensuring solver claims are honest, avoiding unverifiable black-box reasoning, maintaining reproducibility, accurately stating completeness/soundness limits, preventing deceptive benchmark practices, and responsibly documenting known solver or kernel weaknesses. |