JSON Schema is the de facto standard for describing the structure of JSON documents. Reasoning about JSON Schema inclusion - whether every instance satisfying a schema S1 also satisfies a schema S2 -is a key building block for a variety of tasks, including version and API compatibility checks, schema refactoring tools, and large-scale schema corpus analysis. Existing approaches fall into two families: rule-based algorithms that are efficient but incomplete and witness generation-based algorithms that are complete but oftentimes extremely slow. This paper introduces a new approach that reconciles the efficiency of rule-based procedures with the completeness of the witness-generation technique, by enriching the latter with a specialized form of normalization. This refutational normalization paves the way for use-cases that are too hard for current tools. Our experiments with real-world and synthetic schemas show that the refutational normalization greatly advances the state-of-the-art in JSON Schema inclusion checking.

翻译：JSON Schema 是描述 JSON 文档结构的事实标准。关于 JSON Schema 包含——即满足模式 S1 的每个实例是否也满足模式 S2——的推理，是多种任务的关键构建模块，包括版本与 API 兼容性检查、模式重构工具以及大规模模式语料库分析。现有方法分为两类：基于规则的算法，虽然高效但不完备；以及基于见证生成的算法，虽然完备但往往极其缓慢。本文提出一种新方法，通过为后一种技术扩展一种特殊形式的规范化，调和了基于规则过程的效率与见证生成技术的完备性。这种反驳性规范化为当前工具难以处理的用例开辟了道路。我们在真实世界与合成模式上的实验表明，反驳性规范化显著推进了 JSON Schema 包含检查的最新水平。