Newclid
  • Newclid
    • Installation
      • Using uv (recommended)
      • Using pip
      • Building from source
    • Quickstart
    • Documentation
    • Contributing
    • About Newclid

Documentation

  • Building a problem setup
    • JGEX
      • JGEX setup
        • Writing a new problem
        • Ensuring the problem can be built
      • JGEX definitions
        • Legacy definitions
        • New Definitions
      • JGEX problems datasets
        • imo_ag_30
        • jgex_ag_231
        • new_benchmark_50
        • examples
    • Geogebra setup
  • Basic Concepts
    • Newclid Predicates
    • Rules
      • Legacy rules
        • r00 : Perpendiculars give parallel
        • r01 : Definition of circle
        • r02 : Parallel from inclination
        • r03 : Arc determines internal angles
        • r04 : Congruent angles are in a circle
        • r05 : Same arc same chord
        • r06 : Base of half triangle
        • r07 : Thales Theorem I
        • r08 : Right triangles common angle I
        • r09 : Sum of angles of a triangle
        • r10 : Ratio cancellation
        • r11 : Bisector theorem I
        • r12 : Bisector theorem II
        • r13 : Isosceles triangle equal angles
        • r14 : Equal base angles imply isosceles
        • r15 : Arc determines inscribed angles (tangent)
        • r16 : Same arc giving tangent
        • r17 : Central angle vs inscribed angle I
        • r18 : Central angle vs inscribed angle II
        • r19 : Hypotenuse is diameter
        • r20 : Diameter is hypotenuse
        • r21 : Cyclic trapezoid
        • r22 : Bisector Construction
        • r23 : Bisector is perpendicular
        • r24 : Cyclic kite
        • r25 : Diagonals of parallelogram I
        • r26 : Diagonals of parallelogram II
        • r27 : Thales theorem II
        • r28 : Overlapping parallels
        • r29 : Midpoint is an eqratio
        • r30 : Right triangles common angle II
        • r31 : Denominator cancelling
        • r32 : SSS Triangle congruence
        • r33 : SAS Triangle congruence
        • r34 : AA Similarity of triangles (direct)
        • r35 : AA Similarity of triangles (reverse)
        • r36 : ASA Congruence of triangles (direct)
        • r37 : ASA Congruence of triangles (reverse)
        • r38 : SSS Triangle similarity (original)
        • r39 : SAS Triangle similarity (original)
        • r40 : Similarity without scaling
        • r41 : Thales theorem III
        • r42 : Thales theorem IV
      • New rules
        • r43 : Orthocenter theorem
        • r44 : Pappus’s theorem
        • r45 : Simson’s line theorem
        • r46 : Incenter theorem
        • r47 : Circumcenter theorem
        • r48 : Centroid theorem
        • r49 : Recognize center of cyclic (circle)
        • r50 : Recognize center of cyclic (cong)
        • r51 : Midpoint splits in two
        • r52 : Properties of similar triangles (Direct)
        • r53 : Properties of similar triangles (Reverse)
        • r54 : Definition of midpoint
        • r55 : Properties of midpoint (cong)
        • r56 : Properties of midpoint (coll)
        • r57 : Pythagoras theorem
        • r58 : Same chord same arc I
        • r59 : Same chord same arc II
        • r60 : SSS Similarity of triangles (Direct)
        • r61 : SSS Similarity of triangles (Reverse)
        • r62 : SAS Similarity of triangles (Direct)
        • r63 : SAS Similarity of triangles (Reverse)
        • r64 : SSS Congruence of triangles (Direct)
        • r65 : SSS Congruence of triangles (Reverse)
        • r66 : SAS Congruence of triangles (Direct)
        • r67 : SAS Congruence of triangles (Reverse)
        • r68 : Similarity without scaling (Direct)
        • r69 : Similarity without scaling (Reverse)
        • r70 : Projective harmonic conjugate
        • r71 : Resolution of ratios
        • r72 : Disassembling a circle
        • r73 : Definition of a circle
        • r74 : Intersection of angle bisector and perpendicular bisector
        • r75 : Equipartition of segments
        • r76 : Locate midpoint of hypotenuse
        • r77 : Properties of congruent triangles (Direct)
        • r78 : Properties of congruent triangles (Reverse)
        • r79 : Divide congruence equation by segment
        • r80 : Same chord same arc III
        • r81 : Same chord same arc IV
        • r82 : Parallel from collinear
        • r83 : Between condition I
        • r84 : Between condition II
        • r85 : Generalized Pythagorean theorem I
        • r86 : Generalized Pythagorean theorem II
        • r87 : Characterization of circumcenter I
        • r88 : Characterization of circumcenter II
        • r89 : Length of a median of a triangle
        • r90 : Parallelogram law
        • r91 : Equal angles in an isosceles trapezoid
        • r92 : Any diameter of a circle crosses the center
  • Frequently Asked Questions
    • How to run a problem?
    • What are the structures that correspond to geometric concepts?
    • What are the geometric objects in the code?
    • How can I add new definitions?
    • How can I add new rules?
    • What do I get after I run a problem?
    • How is the proof structured?
    • What are justifications?
    • What is the proper way to add an auxiliary point to a problem?

Source code API

  • Newclid
    • GeometricSolver
      • GeometricSolver.animate()
      • GeometricSolver.draw_figure()
      • GeometricSolver.proof()
      • GeometricSolver.run()
      • GeometricSolver.write_all_outputs()
    • GeometricSolverBuilder
      • GeometricSolverBuilder.build()
      • GeometricSolverBuilder.with_deductive_agent()
      • GeometricSolverBuilder.with_deductors()
      • GeometricSolverBuilder.with_rule_matcher()
      • GeometricSolverBuilder.with_rules()
      • GeometricSolverBuilder.with_rules_from_file()
    • Agent
      • Agent Builder
        • make_agent()
      • Agents Interface
        • DeductiveAgent
      • Ddarn
        • DDARNStats
        • DDARN
      • Follow Deductions
        • DeductionType
        • CachedRuleDeduction
        • ARPremiseConstruction
        • CachedARDeduction
        • CachedNumericalCheckDeduction
        • CachedReflexivityDeduction
        • DeductionProvider
        • FollowDeductionsStats
        • FollowDeductions
        • DoubleCheckError
      • Human Agent
        • NamedFunction
        • HumanAgent
    • Animation
      • ProofAnimation
        • ProofAnimation.animate()
      • html_animation()
      • Artists In Animation
        • PointArtists
        • ArtistInAnimation
        • init_point_name_to_artist()
      • Clause
        • ClauseArtists
        • init_clauses_to_draw()
      • Goal
        • GoalArtists
        • init_goals_to_draw()
      • Justifications
        • JustificationArtists
        • JustificationToDraw
        • init_justifications_to_draw()
        • draw_generic_justification()
      • Proof Animation
        • ProofAnimationParts
        • ProofAnimation
      • Text Animation
        • TextAnimation
    • Deductors
      • ARReason
        • ARReason.ANGLE_CHASING
        • ARReason.RATIO_CHASING
      • Sympy Ar
        • Algebraic Manipulator
        • Ar Predicates
        • Ar Table
        • Table Angles
        • Table Ratios
      • Deductor Interface
        • ARCoefficient
        • ARPremise
        • ARDeduction
        • Deductor
        • add_to_deductors()
        • check_from_deductors()
        • justify_from_deductors()
    • Draw
      • Ar Application
        • draw_ar_application()
        • draw_deps_predicates()
      • Figure
        • init_figure()
        • draw_figure()
        • draw_point()
      • Geometries
        • ArtistKwargs
        • draw_circle_symbol()
        • draw_circle()
        • draw_triangle()
        • draw_segment()
        • draw_arrow()
        • draw_complete_arrow()
      • Jgex Constructions
        • draw_jgex_problem_clauses()
        • draw_jgex_constructions()
      • Predicates
        • random()
        • draw_predicate()
        • draw_perp_rectangle()
        • draw_line_symbol()
        • draw_line()
        • draw_free_perpendicular_symbol()
      • Rule
        • draw_rule_application()
        • circumcenter_of_triangle()
      • Theme
        • DrawTheme
        • fill_missing()
    • Ggb
      • Apply Commands Effects
        • apply_commands_effects_on_elements()
      • Assumptions From Commands
        • commands_to_newclid_assumptions()
      • Assumptions From Elements
        • elements_to_newclid_assumptions()
      • Assumptions From Elements Relation
        • relationships_to_newclid_assumptions()
      • Elements Relationships
        • RelationShipType
        • ParaRelationship
        • OrthoRelationship
        • BisectorLineRelationship
        • BisectorPointRelationship
        • TangentRelationship
      • Problem Builder
        • GeogebraProblemBuilder
        • load_ggb_file()
        • GGBSetup
      • Read Commands
        • read_commands()
        • GGBReadCommandType
        • GGBLineCommand
        • GGBParaCommand
        • GGBOrthogonalLineCommand
        • GGBIntersectCommand
        • GGBCircleCommand
        • GGBCircumcircleCommand
        • GGBCompassCommand
        • GGBAddPointOnObjectCommand
        • GGBCenterCommand
        • GGBMidpointCommand
        • GGBAngularBisectorLinesCommand
        • GGBAngularBisectorPointsCommand
        • GGBTangentOnCircleCommand
        • GGBTangentOutsideCircleCommand
        • GGBXMLCommandType
        • GGBXMLCommandComponents
      • Read Elements
        • GGBElementType
        • GGBPoint
        • GGBLine
        • GGBConic
        • read_elements()
      • Relationships From Commands
        • relationships_from_commands()
    • Heuristics
      • HeuristicName
        • HeuristicName.LINE_INTERSECTIONS
        • HeuristicName.CENTERS
        • HeuristicName.ANGLE_VERTICES
        • HeuristicName.MIDPOINT
        • HeuristicName.EQDISTANCE
        • HeuristicName.FOOT
        • HeuristicName.REFLECT_ON_CENTER
        • HeuristicName.THREE_CIRCUMCIRCLES_FOR_EQANGLE_GOAL
      • Heuristic
        • Heuristic.new_clauses()
      • HeuristicSetup
        • HeuristicSetup.model_config
        • HeuristicSetup.points
        • HeuristicSetup.free_points
        • HeuristicSetup.lines
        • HeuristicSetup.circles
        • HeuristicSetup.angles
        • HeuristicSetup.goals
      • Alphabet
        • get_available_from_alphabet()
      • Angle Vertices
        • AngleVerticesHeuristicConfig
        • AngleVerticesHeuristic
      • Apply Heuristics
        • apply_complete_the_picture_heuristics()
        • apply_heuristics_on_nc_problem()
        • build_nc_problem_from_jgex_problem()
      • Centers Of Cyclic
        • CentersOfCyclicHeuristicConfig
        • CentersOfCyclicHeuristic
      • Circumcircles For Eqangle
        • ThreeCircumcirclesForEqangleGoalHeuristicConfig
        • ThreeCircumcirclesForEqangleGoalHeuristic
      • Foots On Lines
        • FootHeuristicConfig
        • FootHeuristic
      • Geometric Objects
        • LineHeuristic
        • CircleHeuristic
        • AngleHeuristic
        • read_geometric_objects_from_predicate_constructions()
      • Heuristic From Config
        • heuristic_from_name()
        • config_from_name()
        • heuristic_from_config()
      • Line Intersections
        • LineIntersectionsHeuristicConfig
        • LineIntersectionsHeuristic
      • Midpoint
        • MidpointHeuristicConfig
        • MidpointHeuristic
      • Reflect On Center
        • ReflectOnCenterHeuristicConfig
        • ReflectOnCenterHeuristic
      • Transfer Distances
        • TransferDistancesHeuristicConfig
        • TransferDistancesHeuristic
    • Jgex
      • Constructions
        • Complete Figure
        • Free
        • Intersections
        • Point On Object
        • Predicate Prescriptions
        • Problem Specific
        • Relative To
      • Angles
        • ang_of()
        • ang_between()
      • Clause
        • JGEXConstruction
        • rename_jgex_construction()
        • is_numerical_argument()
        • JGEXClause
        • order_clauses_by_points_construction_order()
      • Definition
        • SketchConstruction
        • SketchCall
        • v()
        • JGEXDefinition
        • mapping_from_construction()
        • input_points_of_clause()
      • Distances
        • ensure_not_too_close_numerical()
        • ensure_not_too_far_numerical()
      • Errors
        • JGEXConstructionError
        • PointTooCloseError
        • PointTooFarError
        • InvalidIntersectError
      • Formulation
        • JGEXFormulation
        • jgex_formulation_from_txt_file()
        • alphabetize()
      • Geometries
        • LENGTH_UNIT
        • JGEXPoint
        • JGEXGeometry
        • JGEXLine
        • JGEXCircle
        • perpendicular_bisector()
        • solve_quad()
        • intersect()
        • circle_circle_intersection()
        • line_circle_intersection()
        • line_line_intersection()
        • reduce_intersection()
      • Jgex Setup Data
        • PredicateConstructionInSetup
        • JGEXClauseInProof
        • JGEXSetupData
        • jgex_clauses_to_setup_data()
      • Problem Builder
        • JGEXProblemBuilder
      • Sketch
        • sketch()
        • sketch_function_name()
        • sketch_aline()
        • sketch_aline0()
        • sketch_acircle()
        • sketch_amirror()
        • sketch_bisect()
        • sketch_exbisect()
        • sketch_bline()
        • sketch_dia()
        • sketch_tangent()
        • sketch_circle()
        • sketch_cc_tangent()
        • sketch_e5128()
        • random_rfss()
        • head_from()
        • sketch_eq_quadrangle()
        • sketch_iso_trapezoid()
        • sketch_eqangle2()
        • sketch_eqangle3()
        • sketch_eqdia_quadrangle()
        • random_points()
        • sketch_free()
        • sketch_isos()
        • sketch_line()
        • sketch_cyclic()
        • sketch_midp()
        • sketch_pentagon()
        • sketch_pline()
        • sketch_pmirror()
        • sketch_quadrangle()
        • sketch_r_trapezoid()
        • sketch_r_triangle()
        • sketch_rectangle()
        • sketch_reflect()
        • sketch_risos()
        • sketch_rotaten90()
        • sketch_rotatep90()
        • sketch_s_angle()
        • sketch_aconst()
        • sketch_segment()
        • sketch_shift()
        • sketch_square()
        • sketch_isquare()
        • sketch_tline()
        • sketch_trapezoid()
        • sketch_triangle()
        • sketch_triangle12()
        • sketch_trisect()
        • sketch_trisegment()
        • sketch_ieq_triangle()
        • sketch_incenter2()
        • sketch_excenter2()
        • sketch_centroid()
        • sketch_ninepoints()
        • sketch_2l1c()
        • sketch_3peq()
        • sketch_isosvertex()
        • sketch_eqratio()
        • sketch_rconst()
        • sketch_eqratio6()
        • sketch_lconst()
        • sketch_rconst2()
        • sketch_between()
        • sketch_between_bound()
        • sketch_iso_trapezoid2()
        • sketch_acute_triangle()
        • sketch_cc_itangent()
        • sketch_simtri()
        • sketch_simtrir()
        • sketch_contri()
        • sketch_contrir()
        • sketch_test_r20()
        • sketch_test_r25()
        • sketch_l2const()
        • sketch_r2const()
      • To Newclid
        • build_newclid_problem()
        • add_clause_to_problem()
        • JGEXClauseConsequences
        • rename_points_in_clause_consequences()
        • JGEXConstructionConsequences
        • rename_points_in_construction_consequences()
    • Justifications
      • Justification
        • Assumption
        • NumericalCheck
        • Reflexivity
        • DirectConsequence
        • justify_dependency()
      • Justify Predicates
        • justify_predicate()
      • Predicates Graph
        • PredicatesGraph
    • Numerical
      • close_enough()
      • nearly_zero()
      • sign()
      • Check
        • same_clock()
        • clock()
      • Geometries
        • PointNum
        • line_num_from_points()
        • LineNum
        • circle_num_from_points_around()
        • circle_num_from_center_and_point()
        • CircleNum
        • line_line_intersection()
    • Predicates
      • predicate_class_from_type()
      • predicate_from_construction()
      • Circumcenter
        • Circumcenter
      • Collinearity
        • Coll
        • NColl
      • Congruence
        • Cong
      • Constant Angle
        • angle_between_4_points()
        • ConstantAngle
        • ACompute
        • aconst_from_acompute()
      • Constant Length
        • ConstantLength
        • LCompute
        • lconst_from_lcompute()
      • Constant Ratio
        • ConstantRatio
        • RCompute
        • rconst_from_rcompute()
      • Cyclic
        • Cyclic
      • Different
        • Diff
      • Equal Angles
        • EqAngle
      • Equal Ratios
        • EqRatio
      • Equation Angle
        • AngleEquation
      • Equation Length
        • LengthEquation
      • Midpoint
        • MidPoint
      • Obtuse Angle
        • ObtuseAngle
      • Parallelism
        • Para
        • NPara
      • Perpendicularity
        • Perp
        • NPerp
      • Pythagoras
        • PythagoreanPremises
        • PythagoreanConclusions
      • Sameclock
        • SameClock
      • Sameside
        • SameSide
        • NSameSide
      • Squared Constant Length
        • SquaredConstantLength
      • Squared Constant Ratio
        • SquaredConstantRatio
      • Triangles Congruent
        • ContriClock
        • ContriReflect
      • Triangles Similar
        • two_triangles()
        • SimtriClock
        • SimtriReflect
    • Problems
      • Imo
      • Problem
        • CompetitionIds
        • Competition
        • ProblemFormulation
        • Problem
    • Rule Matching
      • Efficient Statement
        • efficient_version()
        • PerpStatement
        • PerpPredicate
        • ParaStatement
        • ParaPredicate
        • EqangleStatement
        • EqanglePredicate
        • EqratioStatement
        • EqratioPredicate
        • CongStatement
        • CongPredicate
        • MidptStatement
        • MidptPredicate
        • TriangleStatement
        • TrianglePredicate
        • CollStatement
        • CollPredicate
        • CircleStatement
        • CirclePredicate
        • CyclicStatement
        • CyclicPredicate
        • generate_permutations()
        • cyclic_perms()
        • coll_perms()
        • circle_perms()
        • triangle_perms()
        • normalize_triangle()
        • normalize_midpt()
        • midpt_perms()
        • normalize_cong()
        • cong_perms()
        • normalize_eqratio()
        • eqratio_perms()
        • normalize_eqangle()
        • eqangle_perms()
        • normalize_para()
        • para_perms()
        • normalize_perp()
        • perp_perms()
        • normalize_coll()
        • normalize_circle()
        • normalize_cyclic()
        • get_representative_of_equivalence_class()
      • Interface
        • RuleMatcher
      • Mapping Matcher
        • MappingMatcher
        • TheoremMapper
        • CCMapper
        • FilterMapper
        • predictates_by_type_name_from_hypergraph()
        • iterate_mapping_with_complementary_assignments()
        • PartialMapping
        • iterate_mappings()
      • Permutations
        • generate_permutations_as_dicts()
    • Symbols
      • Circles Registry
        • CircleSymbol
        • CirclesRegistry
        • CircleMerge
      • Lines Registry
        • LineSymbol
        • LinesRegistry
        • LineMerge
      • Merging Symbols
        • SymbolMergeHistory
        • representent_of()
        • merge_symbols()
      • Points Registry
        • Point
        • PointsRegisty
      • Symbols Registry
        • SymbolsRegistry
    • All Rules
      • DEFAULT_RULES
      • ALL_RULES
      • DEACTIVATED_RULES
      • TRIAGE_NO_RULE_NEEDED
      • TRIAGE_LEAVE_RULE_OUT
    • Api
      • GeometricSolver
        • GeometricSolver.run()
        • GeometricSolver.proof()
        • GeometricSolver.animate()
        • GeometricSolver.draw_figure()
        • GeometricSolver.write_all_outputs()
      • ProblemBuilder
        • ProblemBuilder.build()
      • PythonDefault
        • PythonDefault.default_rule_matcher()
        • PythonDefault.default_deductors()
        • PythonDefault.default_deductive_agent()
        • PythonDefault.callback()
      • GeometricSolverBuilder
        • GeometricSolverBuilder.build()
        • GeometricSolverBuilder.with_deductive_agent()
        • GeometricSolverBuilder.with_rule_matcher()
        • GeometricSolverBuilder.with_deductors()
        • GeometricSolverBuilder.with_rules()
        • GeometricSolverBuilder.with_rules_from_file()
    • Api Defaults
      • APIDefault
        • APIDefault.default_rule_matcher()
        • APIDefault.default_deductors()
        • APIDefault.default_deductive_agent()
        • APIDefault.callback()
    • Cli
      • NewclidOptions
        • NewclidOptions.output_dir
        • NewclidOptions.saturate
        • NewclidOptions.agent
        • NewclidOptions.seed
        • NewclidOptions.log_level
        • NewclidOptions.model_config
      • parse_cli_args()
      • make_cli_parser()
      • LogLevel
        • LogLevel.DEBUG
        • LogLevel.INFO
        • LogLevel.WARNING
        • LogLevel.ERROR
    • Llm Input
      • new_problem_from_llm_aux_output()
      • problem_to_llm_input()
      • problem_to_llm_input_without_predicates()
      • TrainingDatapoint
        • TrainingDatapoint.aux_io
        • TrainingDatapoint.proof_output
        • TrainingDatapoint.from_proof_data()
        • TrainingDatapoint.from_proof_data_aux_combinations()
        • TrainingDatapoint.model_config
      • AuxTrainingDatapoint
        • AuxTrainingDatapoint.input
        • AuxTrainingDatapoint.aux_output
        • AuxTrainingDatapoint.from_setup_data()
        • AuxTrainingDatapoint.from_setup_data_aux_combinations()
        • AuxTrainingDatapoint.model_config
    • Predicate Types
      • PredicateArgument
    • Problem
      • PredicateConstruction
        • PredicateConstruction.string
        • PredicateConstruction.predicate_type
        • PredicateConstruction.args
        • PredicateConstruction.canonicalize()
        • PredicateConstruction.from_tuple()
        • PredicateConstruction.from_str()
        • PredicateConstruction.from_predicate_type_and_args()
        • PredicateConstruction.model_config
      • predicate_from_str()
      • predicate_to_construction()
      • is_numerical_argument()
      • predicate_points()
      • rename_predicate_construction()
      • ProblemSetup
        • ProblemSetup.name
        • ProblemSetup.points
        • ProblemSetup.assumptions
        • ProblemSetup.goals
        • ProblemSetup.check_points_are_unique()
        • ProblemSetup.check_assumptions_and_goals_refer_to_existing_points()
        • ProblemSetup.with_new()
        • ProblemSetup.pretty_str()
        • ProblemSetup.model_config
      • nc_problem_is_valid()
      • rename_points_in_nc_problem()
      • filter_points_from_nc_problem()
    • Proof Data
      • PredicateInProof
        • PredicateInProof.id
        • PredicateInProof.predicate
        • PredicateInProof.model_config
      • ProofStep
        • ProofStep.proven_predicate
        • ProofStep.justification
        • ProofStep.applied_on_predicates
        • ProofStep.model_config
      • ProofData
        • ProofData.proof_length
        • ProofData.proof_rules_length
        • ProofData.points
        • ProofData.proven_goals
        • ProofData.unproven_goals
        • ProofData.construction_assumptions
        • ProofData.model_config
        • ProofData.numerical_checks
        • ProofData.trivial_predicates
        • ProofData.proof_steps
        • ProofData.set_proof_length()
      • proof_data_from_state()
      • proof_justifications_to_proof_data()
    • Proof Justifications
      • goals_justifications()
    • Proof State
      • ProofBuildError
      • ProofState
        • ProofState.match_theorem()
        • ProofState.apply()
        • ProofState.check()
        • ProofState.check_numerical()
        • ProofState.justify()
        • ProofState.check_goals()
    • Proof Writing
      • ProofSections
        • ProofSections.points
        • ProofSections.assumptions
        • ProofSections.numerical_checks
        • ProofSections.trivial_predicates
        • ProofSections.proven_goals
        • ProofSections.unproven_goals
        • ProofSections.proof_steps
        • ProofSections.appendix_ar
        • ProofSections.model_config
      • write_proof()
      • write_proof_sections()
      • CarryOver
        • CarryOver.update()
    • Rng
      • setup_rng()
    • Rule
      • RuleConstruction
        • RuleConstruction.name
        • RuleConstruction.variables
        • RuleConstruction.model_config
      • RuleApplication
        • RuleApplication.predicate
        • RuleApplication.rule
        • RuleApplication.premises
        • RuleApplication.dependency_type
        • RuleApplication.canonicalize()
        • RuleApplication.model_config
      • Rule
        • Rule.model_config
        • Rule.id
        • Rule.description
        • Rule.premises_txt
        • Rule.conclusions_txt
        • Rule.allow_point_repetition
        • Rule.premises
        • Rule.conclusions
        • Rule.fullname
        • Rule.variables
      • rules_from_file()
      • rules_from_txt()
    • Run Loop
      • RunInfos
        • RunInfos.runtime
        • RunInfos.success
        • RunInfos.steps
        • RunInfos.success_per_goal
        • RunInfos.agent_stats
        • RunInfos.model_config
      • run_loop()
    • Tools
      • InfQuotientError
      • get_quotient()
      • atomize()
      • str_to_fraction()
      • fraction_to_len()
      • fraction_to_ratio()
      • fraction_to_angle()
      • reshape()
      • add_edge()
      • run_static_server()
      • boring_predicate()
      • point_construction_tuple()
      • points_by_construction_order()
      • pretty_basemodel_diff()
      • pretty_basemodel_list_diff()
    • Webapp
      • pull_to_server()
  • Ncdgen
    • Aux Discriminators
      • discriminator_from_name()
      • He Point Deps
        • AuxFromHEPointsDeps
      • Newclid Traceback
        • AuxFromNewclidTraceback
    • Constructions
      • ConstructionDefinition
        • ConstructionDefinition.in_args
        • ConstructionDefinition.out_args
        • ConstructionDefinition.n_required_points
        • ConstructionDefinition.model_config
      • load_constructions()
    • Build Diagram
      • SubproblemSummaryStats
        • SubproblemSummaryStats.skipped_not_enough_rules_applications_subproblems
        • SubproblemSummaryStats.unhandled_failure_to_build_subproblem_count
        • SubproblemSummaryStats.skipped_blacklisted_aux_setup_pairs
        • SubproblemSummaryStats.model_config
      • FailedClauseAttempt
        • FailedClauseAttempt.problem
        • FailedClauseAttempt.clause
        • FailedClauseAttempt.attempt_time
        • FailedClauseAttempt.model_config
      • DiagramGenerationMetadata
        • DiagramGenerationMetadata.run_uuid
        • DiagramGenerationMetadata.diagram_uuid
        • DiagramGenerationMetadata.is_predefined_diagram
        • DiagramGenerationMetadata.config
        • DiagramGenerationMetadata.diagram_construction_time_sec
        • DiagramGenerationMetadata.diagram_succeeded
        • DiagramGenerationMetadata.saturation_succeeded
        • DiagramGenerationMetadata.saturation_time_sec
        • DiagramGenerationMetadata.agent_saturation_stats
        • DiagramGenerationMetadata.failed_clause_attempts
        • DiagramGenerationMetadata.created_at
        • DiagramGenerationMetadata.subproblem_summary_stats
        • DiagramGenerationMetadata.model_config
      • Diagram
        • Diagram.solver
        • Diagram.problem
        • Diagram.dependencies
        • Diagram.setup_graph
        • Diagram.solver
        • Diagram.jgex_problem
        • Diagram.nc_problem
        • Diagram.setup_graph
        • Diagram.jgex_clauses_consequences
      • build_diagram()
      • setupgraph()
    • Double Checking
      • SingleDoubleCheckStatistics
        • SingleDoubleCheckStatistics.setup_clauses
        • SingleDoubleCheckStatistics.aux_clauses_used
        • SingleDoubleCheckStatistics.aux_clauses_unused
        • SingleDoubleCheckStatistics.alpha_mapping
        • SingleDoubleCheckStatistics.run_infos
        • SingleDoubleCheckStatistics.double_check_setup
        • SingleDoubleCheckStatistics.double_check_proof
        • SingleDoubleCheckStatistics.model_config
      • DoubleCheckStatistics
        • DoubleCheckStatistics.single_double_check_stats
        • DoubleCheckStatistics.model_config
        • DoubleCheckStatistics.true_aux_clauses
        • DoubleCheckStatistics.false_positive_aux_clauses
        • DoubleCheckStatistics.final_proof
        • DoubleCheckStatistics.training_data
      • do_double_check()
      • points_requirements_graph_from_jgex_clauses()
    • Extract Datapoint
      • SubProblemDatapoint
        • SubProblemDatapoint.double_check_statistics
        • SubProblemDatapoint.subproblem_str
        • SubProblemDatapoint.alphabetized_subproblem_str
        • SubProblemDatapoint.sub_problem_proof
        • SubProblemDatapoint.level_predicate_count
        • SubProblemDatapoint.solution_natural_language
        • SubProblemDatapoint.model_config
        • SubProblemDatapoint.larger_problem
        • SubProblemDatapoint.larger_nc_problem
        • SubProblemDatapoint.has_double_checked_aux_construction
      • generate_subproblems_datapoints()
    • Extract Subproblems
      • extract_subproblems_and_their_dependencies()
    • Generation Configuration
      • IntersectCases
        • IntersectCases.INTERSECT
        • IntersectCases.OTHER
      • DiagramGenerationConfig
        • DiagramGenerationConfig.min_pts
        • DiagramGenerationConfig.max_pts
        • DiagramGenerationConfig.initial_jgex_problem
        • DiagramGenerationConfig.output_gcs_file
        • DiagramGenerationConfig.emit_only_double_checked_aux_subproblems
        • DiagramGenerationConfig.aux_discriminator
        • DiagramGenerationConfig.debug
        • DiagramGenerationConfig.debug_problem
        • DiagramGenerationConfig.double_check_probability
        • DiagramGenerationConfig.skip_aux_setup_pairs_previous_false_positive
        • DiagramGenerationConfig.min_rules_applied
        • DiagramGenerationConfig.random_seed
        • DiagramGenerationConfig.attempts_per_diagram_build
        • DiagramGenerationConfig.max_check_per_predicate
        • DiagramGenerationConfig.construction_counter_reporting_rate
        • DiagramGenerationConfig.attempts_per_clause
        • DiagramGenerationConfig.aux_tag
        • DiagramGenerationConfig.pmf_additional_free_points_sweep
        • DiagramGenerationConfig.model_config
        • DiagramGenerationConfig.pmf_intersect_vs_other_sweep
        • DiagramGenerationConfig.pmf_num_intersecting_to_sample_sweep
        • DiagramGenerationConfig.run_uuid
        • DiagramGenerationConfig.timeout
        • DiagramGenerationConfig.n_workers
        • DiagramGenerationConfig.jsonl_dump_file
        • DiagramGenerationConfig.log_level
        • DiagramGenerationConfig.validate_pmf_sweep()
        • DiagramGenerationConfig.validate_output_gcs_file()
        • DiagramGenerationConfig.validate_min_max_pts()
      • SweepSelection
        • SweepSelection.model_config
        • SweepSelection.additional_free_points_sweep_selection
        • SweepSelection.intersect_vs_other_sweep_selection
        • SweepSelection.num_intersecting_to_sample_sweep_selection
      • sample_sweep_parameters()
    • Generation Loop
      • Datapoint
        • Datapoint.subproblem
        • Datapoint.generation_metadata
        • Datapoint.model_config
      • run_data_generation_loop()
    • Hydra Config
      • hydra_to_pydantic_generation_config()
    • Read Datapoints
      • read_datapoints_from_file()
    • Sampling
      • sample_from_pmf()
      • sample_order_from_pmf()
      • combinations_in_random_order()
    • Solver
      • SolverInterface
        • SolverInterface.solve_problem()
      • SolverError
      • NewclidSolver
        • NewclidSolver.solve_problem()
    • Testing
      • StubJGEXSolver
        • StubJGEXSolver.with_outputs_for_problem_clauses()
        • StubJGEXSolver.solve_problem()
Newclid
  • Newclid
  • Justifications
  • View page source
Previous Next

Justifications

Define enumeration of different kinds of justifications of predicates.

  • Justification
    • Assumption
      • Assumption.predicate
      • Assumption.dependency_type
      • Assumption.model_config
    • NumericalCheck
      • NumericalCheck.predicate
      • NumericalCheck.dependency_type
      • NumericalCheck.model_config
    • Reflexivity
      • Reflexivity.predicate
      • Reflexivity.dependency_type
      • Reflexivity.model_config
    • DirectConsequence
      • DirectConsequence.predicate
      • DirectConsequence.model_config
      • DirectConsequence.premises
      • DirectConsequence.dependency_type
    • justify_dependency()
  • Justify Predicates
    • justify_predicate()
  • Predicates Graph
    • PredicatesGraph
      • PredicatesGraph.has_edge()
      • PredicatesGraph.predicates
      • PredicatesGraph.premises()
      • PredicatesGraph.save_pyvis()
Previous Next

© Copyright 2024-2025, Mathïs Fédérico, Vladmir Sicca, Tianxiang Xia, Yury Kudryashov, Harmonic.fun.

Built with Sphinx using a theme provided by Read the Docs.