Pull requests - nitta-lab/RDLProofSystem

Fork: 0

nitta-lab / RDLProofSystem

...

41 commits

81 files changed

0 commit comments

2 contributors

Commits on 2026-11-08

Sakoda2269	Merge branch 'feature/axiom-inference-mk2' of github.com:Sakoda2269/RDLPrototype into feature/axiom-inference-mk2	874792a
Sakoda2269	map compositionの推論を作成	5384714

Commits on 2026-11-02

Sakoda2269

Merge branch 'main' into feature/axiom-inference-mk2

7804d3d

Commits on 2026-10-25

Sakoda2269	テストを修正	1d63340
Sakoda2269	細かなバグを修正	344f328
Sakoda2269	依存関係の推論実装完了	73a7ac2
Sakoda2269	再帰的に公理を適用するように変更	87b773d
Sakoda2269	依存関係の推論のテスト中	c696b33
Sakoda2269	依存関係の推論を実装	38dd22e
Sakoda2269	細かな不具合を修正	9854c8b
Sakoda2269	merge origin	755b909
Sakoda2269	初期化を追加	7adbd54

Commits on 2026-10-21

Sakoda2269

dependencyの推論実装中

08e8a3a

Commits on 2026-10-01

Sakoda2269

公理実装完了

ca2e140

Commits on 2026-09-30

Sakoda2269	ArgumentExtensionまで	ddbd519
Sakoda2269	test完了	25fc879
Sakoda2269	isMatchedByにPositionを追加	2da711b
Sakoda2269	InTestを削除	1c98c0c
Sakoda2269	Uncurrying途中まで	e64b8e1

Commits on 2026-09-29

Sakoda2269	Constantnessまで	ce2914c
Sakoda2269	Constantness途中	e42621e
Sakoda2269	testを修正	3264627

Commits on 2026-09-28

Sakoda2269

testを修正, EquationAxiom#applyの戻り値を変更

6ac7030

Commits on 2026-09-25

Sakoda2269

公理更新中

09b8a70

Commits on 2026-09-23

Sakoda2269	公理見直し中	6062811
Sakoda2269	公理の推論の実装変更とtransitivity testまで	95d24b7

Commits on 2026-09-22

Sakoda2269	requiredAssumptions実装まで	d8a6590
Sakoda2269	in, codomain membership, domain membershipを実装	8fbdd2d

Commits on 2026-09-21

Sakoda2269	公理系一通り実装完了	0dd6a29
Sakoda2269	Right Normalizationまで	2fc8d7a

Commits on 2026-09-18

Sakoda2269	ArgumentDependencyExtractionまで	bc1b3eb
Sakoda2269	Merge branch 'main' into feature/axiom-inference-mk2	777ecf7
Sakoda2269	MapComposition 途中まで	998595c
Sakoda2269	dependency axiom unccuried mappingまで	886fd4a

Commits on 2026-09-17

Sakoda2269

left sub, identityを追加

3089673

Commits on 2026-09-16

Sakoda2269	right sub実装まで	424ec91
Sakoda2269	dynamicのsubstitutionを作成	46c8b72
Sakoda2269	isMatchedByからdepthを削除	9f6f003
Sakoda2269	merge main	1a55b15

Commits on 2026-09-14

Sakoda2269	dynamicTermのisMatchedByまで	b9eb38e
Sakoda2269	dynami 修正　途中まで	10574c8

Patch

Unified Split

Showing 81 changed files

Ignore Space Show notes View src/main/java/Main.java

Ignore Space Show notes View src/main/java/exceptions/MissingContextException.java 0 → 100644

Ignore Space Show notes View src/main/java/exceptions/ReplaceFailedException.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/AssumptionSizeCalculator.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/ConclusionSizeCalculator.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/DependencyAxiom.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/EquationAxiom.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/In.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/InferenceHistory.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/InferenceHistoryNode.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/InferenceOrderConstraint.java

Ignore Space Show notes View src/main/java/inference/InferenceRule.java

Ignore Space Show notes View src/main/java/inference/ProofState.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/ProofSystem.java

Ignore Space Show notes View src/main/java/inference/axioms/ArgumentConstraint.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/ArgumentExtension.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/ArgumentReduction.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/CompositeMapping.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/ConstantMapping.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/Constantness.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/DependencyExtension.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/Identity.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/LeftSubstitution.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/MapComposition.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/PseudoConstantness.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/RightNormalization.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/RightSubstitution.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/UncurriedMapping.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/axioms/Uncurrying.java 0 → 100644

Ignore Space Show notes View src/main/java/inference/equivalence/SemanticEquivalenceRelation.java

Show notes View src/main/java/inference/rewrite/Position.java 100644 → 0

Ignore Space Show notes View src/main/java/inference/rewrite/ResourceTree.java

Ignore Space Show notes View src/main/java/inference/rewrite/RewriteInferenceSystem.java

Ignore Space Show notes View src/main/java/models/Position.java 0 → 100644

Ignore Space Show notes View src/main/java/models/algebra/Position.java

Ignore Space Show notes View src/main/java/models/formulas/DependencyFormula.java

Ignore Space Show notes View src/main/java/models/formulas/EquationFormula.java

Ignore Space Show notes View src/main/java/models/formulas/meta/MetaDependencyFormula.java

Ignore Space Show notes View src/main/java/models/formulas/meta/MetaEquationFormula.java

Ignore Space Show notes View src/main/java/models/formulas/meta/MetaFormula.java

Ignore Space Show notes View src/main/java/models/terms/Dependency.java

Ignore Space Show notes View src/main/java/models/terms/DependencyTerm.java

Show notes View src/main/java/models/terms/PrimedTerm.java 100644 → 0

Ignore Space Show notes View src/main/java/models/terms/RDLTerm.java

Ignore Space Show notes View src/main/java/models/terms/Resource.java

Ignore Space Show notes View src/main/java/models/terms/ResourceConstant.java

Ignore Space Show notes View src/main/java/models/terms/meta/MatchConstraint.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaConstant.java 0 → 100644

Ignore Space Show notes View src/main/java/models/terms/meta/MetaDependency.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaDependencyTerm.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaDependencyTermVariable.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaDependencyVariable.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaDynamicDependency.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java 0 → 100644

Ignore Space Show notes View src/main/java/models/terms/meta/MetaDynamicTerm.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaEvaluatableTermVariable.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaRDLTerm.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaRDLTermVariable.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaResource.java

Ignore Space Show notes View src/main/java/models/terms/meta/MetaTermGenerator.java

Show notes View src/main/java/models/terms/meta/MetaTermPairGenerator.java 100644 → 0

Ignore Space Show notes View src/main/java/models/terms/meta/MetaVariable.java

Show notes View src/main/java/utils/ExpressionUitls.java 100644 → 0

Ignore Space Show notes View src/main/java/utils/ExpressionUtils.java 0 → 100644

Ignore Space Show notes View src/test/java/inference/DependencyInferenceTest.java 0 → 100644

Ignore Space Show notes View src/test/java/inference/ProofSystemTest.java 0 → 100644

Ignore Space Show notes View src/test/java/inference/inferencerule/DependencyAxiomTest.java 0 → 100644

Ignore Space Show notes View src/test/java/inference/inferencerule/EqualityAxiomTest.java 0 → 100644

Show notes View src/test/java/inferencerule/DependencyAxiomTest.java 100644 → 0

Show notes View src/test/java/inferencerule/EqualityAxiomTest.java 100644 → 0

Show notes View src/test/java/inferencerule/InferenceRuleTest.java 100644 → 0

Ignore Space Show notes View src/test/java/rewrite/RewriteInferenceTest.java

Ignore Space Show notes View src/test/java/terms/DependencyTermTest.java

Ignore Space Show notes View src/test/java/terms/DependencyTest.java

Ignore Space Show notes View src/test/java/terms/meta/MetaDependencyTermTest.java

Ignore Space Show notes View src/test/java/terms/meta/MetaDependencyTest.java

Ignore Space Show notes View src/test/java/terms/meta/MetaDynamicDependencyTermTest.java 0 → 100644

Ignore Space Show notes View src/test/java/terms/meta/MetaDynamicDependencyTest.java 0 → 100644

Show notes View src/test/java/terms/meta/MetaDynamicTermTest.java 100644 → 0

Ignore Space Show notes View src/test/java/terms/meta/MetaResourceVariableTest.java

Ignore Space Show notes View src/test/java/utils/Utils.java