Newclid

Contents:

  • Overview
    • Proof State
    • Deductive Agent
    • How is a Problem Built
    • Problem Solving
      • Matching and Caching
    • Writing the Proof
      • Translating to natural language
  • Python interface
  • Adding new problems
    • Using definitions
    • Writing a new problem
    • Ensuring the problem can be built
  • Adding new rules
  • Default Files
    • Definitions
      • Legacy definitions
        • angle_bisector x a b c
        • angle_mirror x a b c
        • circle x a b c
        • circumcenter x a b c
        • eq_quadrangle a b c d
        • iso_trapezoid a b c d
        • eq_triangle x b c
        • eqangle2 x a b c
        • eqdia_quadrangle a b c d
        • eqdistance x a b c
        • foot x a b c
        • free a
        • incenter x a b c
        • incenter2 x y z i a b c
        • excenter x a b c
        • excenter2 x y z i a b c
        • centroid x y z i a b c
        • ninepoints x y z i a b c
        • intersection_cc x o w a
        • intersection_lc x a o b
        • intersection_ll x a b c d
        • intersection_lp x a b c m n
        • intersection_lt x a b c d e
        • intersection_pp x a b c d e f
        • intersection_tt x a b c d e f
        • iso_triangle a b c
        • lc_tangent x a o
        • midpoint x a b
        • mirror x a b
        • nsquare x a b
        • on_aline x a b c d e
        • on_bline x a b
        • on_circle x o a
        • on_line x a b
        • on_pline x a b c
        • on_tline x a b c
        • orthocenter x a b c
        • parallelogram a b c x
        • pentagon a b c d e
        • psquare x a b
        • quadrangle a b c d
        • r_trapezoid a b c d
        • r_triangle a b c
        • rectangle a b c d
        • reflect x a b c
        • risos a b c
        • segment a b
        • shift x b c d
        • square a b x y
        • isquare a b c d
        • trapezoid a b c d
        • triangle a b c
        • triangle12 a b c
        • 2l1c x y z i a b c o
        • e5128 x y a b c d
        • 3peq x y z a b c
        • trisect x y a b c
        • trisegment x y a b
        • on_dia x a b
        • ieq_triangle a b c
        • cc_tangent x y z i o a w b
        • eqangle3 x a b d e f
        • tangent x y a o b
        • on_circum x a b c
      • New Definitions
        • on_pline0 x a b c
        • iso_triangle0 a b c
        • iso_triangle_vertex x b c
        • iso_triangle_vertex_angle x b c
        • on_aline0 x a b c d e f g
        • eqratio x a b c d e f g
        • eqratio6 x a c e f g h
        • rconst a b c x r
        • rconst2 x a b r
        • aconst a b c x r
        • s_angle a b x y
        • lconst x a l
    • 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 : Hypothenuse 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)
  • Problems Datasets
    • imo_ag_30
    • jgex_ag_231
    • new_benchmark_50
    • examples
  • Newclid
    • Agent
      • Agents Interface
        • DeductiveAgent
      • Ddarn
        • DDARN
      • Human Agent
        • NamedFunction
        • HumanAgent
    • Algebraic Reasoning
      • Algebraic Manipulator
        • AlgebraicManipulator
      • Tables
        • strip()
        • plus()
        • plus_all()
        • mult()
        • minus()
        • recon()
        • replace()
        • report()
        • Table
    • Dependencies
      • Dependency
        • NumericalyFalseDependencyError
        • Dependency
      • Dependency Graph
        • DependencyGraph
      • Symbols
        • Symbol
        • Point
        • Line
        • Circle
      • Symbols Graph
        • SymbolsGraph
    • Formulations
      • Clause
        • Clause
        • translate_sentence()
      • Definition
        • DefinitionJGEX
      • Problem
        • ProblemJGEX
      • Rule
        • Rule
    • Numerical
      • close_enough()
      • nearly_zero()
      • sign()
      • Angles
        • ang_of()
        • ang_between()
      • Check
        • same_clock()
        • clock()
      • Distances
        • PointTooCloseError
        • PointTooFarError
        • check_too_close_numerical()
        • check_too_far_numerical()
      • Draw Figure
        • init_figure()
        • draw_figure()
        • fill_missing()
        • draw_circle()
        • draw_line()
        • draw_segment()
        • draw_segment_num()
        • draw_angle()
        • draw_rectangle()
        • draw_point()
      • Geometries
        • PointNum
        • FormNum
        • LineNum
        • CircleNum
        • perpendicular_bisector()
        • InvalidIntersectError
        • InvalidReduceError
        • solve_quad()
        • intersect()
        • circle_circle_intersection()
        • line_circle_intersection()
        • circle_segment_intersect()
        • line_line_intersection()
        • reduce()
      • Sketch
        • sketch()
        • 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()
    • Predicates
      • Circumcenter
        • Circumcenter
      • Collinearity
        • Coll
        • NColl
      • Congruence
        • Cong
      • Constant Angle
        • ConstantAngle
        • ACompute
      • Constant Length
        • ConstantLength
        • LCompute
      • Constant Ratio
        • ConstantRatio
        • RCompute
      • Cyclic
        • Cyclic
      • Different
        • Diff
      • Equal Angles
        • EqAngle
      • Equal Ratios
        • EqRatio
        • EqRatio3
      • Midpoint
        • MidPoint
      • Parallelism
        • Para
        • NPara
      • Perpendicularity
        • Perp
        • NPerp
      • Predicate
        • Predicate
      • Pythagoras
        • PythagoreanPremises
        • PythagoreanConclusions
      • Sameclock
        • SameClock
      • Sameside
        • SameSide
        • NSameSide
      • Triangles Congruent
        • ContriClock
        • ContriReflect
      • Triangles Similar
        • two_triangles()
        • SimtriClock
        • SimtriReflect
    • Api
      • GeometricSolver
        • GeometricSolver.run()
        • GeometricSolver.write_proof_steps()
        • GeometricSolver.draw_figure()
        • GeometricSolver.write_run_infos()
        • GeometricSolver.write_all_outputs()
      • GeometricSolverBuilder
        • GeometricSolverBuilder.defs
        • GeometricSolverBuilder.rules
        • GeometricSolverBuilder.build()
        • GeometricSolverBuilder.load_problem_from_file()
        • GeometricSolverBuilder.load_problem()
        • GeometricSolverBuilder.del_goals()
        • GeometricSolverBuilder.load_problem_from_txt()
        • GeometricSolverBuilder.load_rules_from_txt()
        • GeometricSolverBuilder.load_rules_from_file()
        • GeometricSolverBuilder.load_defs_from_file()
        • GeometricSolverBuilder.load_defs_from_txt()
        • GeometricSolverBuilder.with_deductive_agent()
        • GeometricSolverBuilder.load_geogebra()
        • GeometricSolverBuilder.load_goal()
        • GeometricSolverBuilder.load_goals_file()
        • GeometricSolverBuilder.with_problem_path()
        • GeometricSolverBuilder.without_figure()
    • Configs
      • default_configs_path()
      • default_defs_path()
      • default_rules_path()
    • Load Geogebra
      • Form
        • Form.Circle
        • Form.Line
      • dedup()
      • load_geogebra()
    • Match Theorems
      • Matcher
        • Matcher.update()
        • Matcher.cache_theorem()
        • Matcher.match_theorem()
    • Proof
      • ConstructionError
      • ProofState
        • ProofState.add_construction()
        • ProofState.build_problemJGEX()
        • ProofState.match_theorem()
        • ProofState.apply_dep()
        • ProofState.check_goals()
    • Proof Writing
      • write_proof_steps()
    • Run Loop
      • run_loop()
    • Statement
      • Statement
        • Statement.check()
        • Statement.check_numerical()
        • Statement.why()
        • Statement.from_tokens()
        • Statement.pretty()
        • Statement.with_new()
        • Statement.draw()
    • Tools
      • InfQuotientError
      • notNone()
      • get_quotient()
      • atomize()
      • str_to_fraction()
      • fraction_to_len()
      • fraction_to_ratio()
      • fraction_to_angle()
      • reshape()
      • add_edge()
      • runtime_cache_path()
      • run_static_server()
      • boring_statement()
    • Webapp
      • pull_to_server()
Newclid
  • Newclid
  • Formulations
  • View page source
Previous Next

Formulations

  • Clause
    • Clause
      • Clause.points
      • Clause.sentences
      • Clause.parse_line()
      • Clause.renamed()
    • translate_sentence()
  • Definition
    • DefinitionJGEX
      • DefinitionJGEX.declare
      • DefinitionJGEX.rely
      • DefinitionJGEX.require
      • DefinitionJGEX.basics
      • DefinitionJGEX.numerics
      • DefinitionJGEX.parse_txt_file()
      • DefinitionJGEX.parse_text()
      • DefinitionJGEX.from_str()
      • DefinitionJGEX.to_dict()
  • Problem
    • ProblemJGEX
      • ProblemJGEX.name
      • ProblemJGEX.constructions
      • ProblemJGEX.goals
      • ProblemJGEX.parse_txt_file()
      • ProblemJGEX.from_text()
      • ProblemJGEX.from_file()
      • ProblemJGEX.with_more_construction()
      • ProblemJGEX.renamed()
      • ProblemJGEX.points()
  • Rule
    • Rule
      • Rule.descrption
      • Rule.premises
      • Rule.conclusions
      • Rule.parse_txt_file()
      • Rule.parse_text()
      • Rule.from_string()
      • Rule.variables()
Previous Next

© Copyright 2024, Mathïs Fédérico, Vladmir Sicca, Tianxiang Xia.

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