summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2024-08-27ambigus parse fix. The proof goal must be changed,Simon-Kor
since now some could define a function with overlapping and worng subdomains
2024-08-27Experimental working commit, programm will compileSimon-Kor
But the Proof that the domain of the local function is not right. Also if in the definition of our local function we just use f(x) = x then we get a technical ambigus parse
2024-08-26Implemented the checking for local functions.Simon-Kor
2024-08-26Non finished attemped to translate a localSimon-Kor
function defintion from abstract to internal
2024-08-26I implemented a parsing rule in concrete.hsSimon-Kor
for local functions and a abstract type in abstract.hs for the proof data structure.
2024-08-24First atemped to write a new way of local function defintionSimon-Kor
2024-08-24hlint suggestionSimon-Kor
2024-08-24Added/Fixed commentsSimon-Kor
2024-08-24naproch sty extensionSimon-Kor
2024-08-14some wishes for NaprocheZFSimon-Kor
2024-08-14The added proposition and definition should haveSimon-Kor
resloved some proofing complications, but they can prove flase together with lemmas about ordinal, the exat lemma are in urysohn.tex at line 522.
2024-08-13less urysohnSimon-Kor
2024-08-12way way way way more urysohnSimon-Kor
2024-08-12way way way more urysohnSimon-Kor
2024-08-12way way more urysohnSimon-Kor
2024-08-12way more urysohnSimon-Kor
2024-08-12Completed the structure of the proof of Urysohn.Simon-Kor
Now every single step has to be proven.
2024-08-12more more way more urysohnSimon-Kor
2024-08-11more more more urysohnSimon-Kor
2024-08-10more more urysohnSimon-Kor
2024-08-10more urysohnSimon-Kor
2024-08-10more ur<sohnSimon-Kor
2024-08-09fixed axiomatic errorSimon-Kor
2024-08-09put cardinalit to the right placeSimon-Kor
2024-08-07Created first urysohn formalizationSimon-Kor
2024-07-23Formattingadelon
2024-07-23Update prover answer prefixesadelon
2024-07-23Update readme.mdadelon
2024-07-21Further Formalisation on numbersSimon-Kor
2024-07-06Formalisation of rationals.Simon-Kor
2024-07-06Formalisation of integers.Simon-Kor
2024-07-06Finished the formalization of naturals.Simon-Kor
2024-07-05Proof of 1 is identity on the naturals and beginSimon-Kor
of Disstributiv law naturals proof
2024-07-02Further Formalisation of naturals.Simon-Kor
Such as induction on naturals and addition laws.
2024-07-02Definition and axioms of naturals.Simon-Kor
2024-06-26Merge remote-tracking branch 'upstream/main' into formalisation_numbersSimon-Kor
2024-06-26update gitigonreSimon-Kor
2024-06-26Working at the numbers.texSimon-Kor
2024-06-25Add `\neg`adelon
2024-06-25Update equivalence.texadelon
2024-06-25[Stable] Implented continuous.tex and omitted some provesSimon-Kor
All changes till here are done such that the check of everything.tex will be a success. There are no logic flaws and false can't be proven with everything out of everthing.tex
2024-06-25Improvement for the ATP proof timeSimon-Kor
2024-06-25Improvement for the ATP proof timeSimon-Kor
2024-06-25Sorted the structure of numbers.texSimon-Kor
2024-06-25definition of equivalence_from_partition can proof false in everything.texSimon-Kor
2024-06-20[Stable] Topologgical-space.texSimon-Kor
2024-06-20[Report] Task failed and was proven in the same time.Simon-Kor
The Line 182 has the goal to apply regular in a topological space. But if i try to prove it with Naproche ZF, then the task will be proven and the task fails in the same time. Console Output is the following: time stack exec zf -- --log library/topology/separation.tex -t 30 --dump ./dump [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fx,fB)&subseteq(fB,setminus(s__carrier(fX),fA))&subseteq(setminus(s__carrier(fX),fA),fU)). [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,setminus(s__carrier(fX),setminus(s__carrier(fX),fU))=fU). [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XN]:(elem(XN,neighbourhoods(fx,fX))&subseteq(XN,fU)&is_closed_in(XN,fX))). [Info] 00:00.21 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,(is_regular(fX)&is_kolmogorov(fX))<=>![XU]:(elem(XU,s__opens(fX))=>![Xx]:(elem(Xx,XU)=>?[XN]:(elem(XN,neighbourhoods(Xx,fX))&subseteq(XN,XU)&is_closed_in(XN,fX))))). [Info] 00:02.34 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))). [Info] 00:02.55 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(fB,setminus(s__carrier(fX),fA))). [Info] 00:08.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,closeds(fX))&elem(fx,fN)&subseteq(fN,fU)). [Info] 00:10.70 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(setminus(s__carrier(fX),fA),setminus(s__carrier(fX),setminus(s__carrier(fX),fU)))). [Info] 00:10.98 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,neighbourhoods(fx,fX))). Verification failed: prover found countermodel fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))).fof(is_regular,axiom,![XX]:(is_regular(XX)<=>![XV]:![Xp,XC]:((elem(Xp,s__carrier(XX))&~elem(Xp,XC)&elem(XC,closeds(XX)))=>?[XU,XC]:(elem(XU,s__opens(XX))&elem(XC,s__opens(XX))&elem(Xp,XU)&subseteq(XC,XV)&inter(XU,XV)=emptyset)))). fof(eqvilance_teethree_closed_neighbourhood_in_open1,axiom,elem(fx,s__carrier(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open2,axiom,~elem(fx,fC)). fof(eqvilance_teethree_closed_neighbourhood_in_open3,axiom,elem(fC,closeds(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open4,axiom,fC=setminus(s__carrier(fX),fU)). fof(eqvilance_teethree_closed_neighbourhood_in_open5,axiom,elem(fx,fU)). fof(eqvilance_teethree_closed_neighbourhood_in_open6,axiom,elem(fU,s__opens(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open7,axiom,is_regular(fX)&is_kolmogorov(fX)). fof(eqvilance_teethree_closed_neighbourhood_in_open8,axiom,inhabited(fX)). fof(eqvilance_teethree_closed_neighbourhood_in_open9,axiom,topological_space(fX)). real 0m14.914s user 0m37.867s sys 0m1.956s
2024-06-18Merge remote-tracking branch 'upstream/main'Simon-Kor
2024-06-18Definition of T3 and regular spaces.Simon-Kor
2024-06-18Update topological-space.texadelon
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-06 14:37:29 +0000