coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
파일 탐색기
최종 버전 다운로드 (.zip)- build.yml
- ACM2_to_BI.v
- encoding.v
- hbi.v
- hil.v
- lbi.v
- tps.v
- utils.v
- BI.md
- BI.v
- BI_undec.v
- CFPI_to_CFI.v
- CFPP_to_CFP.v
- PCP_to_CFPI.v
- PCP_to_CFPP.v
- Facts.v
- CFG.v
- CFG_undec.v
- CFP.v
- CFP_undec.v
- HaltTM_1_to_CM1_HALT.v
- MM2_HALTING_to_CM1_HALT.v
- CM1_facts.v
- CM1.v
- CM1_undec.v
- FRACTRAN_to_H10C_SAT.v
- H10C_SAT_to_H10SQC_SAT.v
- H10SQC_SAT_to_H10UC_SAT.v
- H10UC_SAT_to_H10UPC_SAT.v
- h10c_utils.v
- H10UPC_facts.v
- H10C.v
- H10C_undec.v
- DeductionFacts.v
- FA.v
- NatModel.v
- PA.v
- Robinson.v
- Signature.v
- TarskiFacts.v
- FragmentND.v
- FragmentNDConsistency.v
- FragmentNDFacts.v
- FullND.v
- FullNDConsistency.v
- FullNDFacts.v
- binZF_to_binFST.v
- FSATd_to_FSATdc.v
- H10p_to_FA.v
- H10UPC_to_FOL.v
- H10UPC_to_FOL_constructions.v
- H10UPC_to_FOL_friedman.v
- H10UPC_to_FOL_full_fragment.v
- H10UPC_to_FOL_minimal.v
- H10UPC_to_FSAT.v
- PCPb_to_binZF.v
- PCPb_to_FOL.v
- PCPb_to_FOL_class.v
- PCPb_to_FOL_intu.v
- PCPb_to_FSAT.v
- PCPb_to_FST.v
- PCPb_to_FSTD.v
- PCPb_to_HF.v
- PCPb_to_HFD.v
- PCPb_to_minZF.v
- PCPb_to_minZFeq.v
- PCPb_to_ZF.v
- PCPb_to_ZFD.v
- PCPb_to_ZFeq.v
- TRAKHTENBROT_to_FSAT.v
- ZF_to_FST.v
- ZF_to_HF.v
- DoubleNegation.v
- Fragment.v
- Full.v
- Listability.v
- FragmentCore.v
- FragmentSoundness.v
- FragmentToTarski.v
- FragmentCore.v
- FragmentFacts.v
- FragmentSoundness.v
- FullCore.v
- FullFacts.v
- FullSoundness.v
- Aczel.v
- Aczel_CE.v
- Aczel_TD.v
- FST_model.v
- HF_model.v
- ZF_conservativity.v
- ZF_model.v
- binFST.v
- binZF.v
- FST.v
- minZF.v
- Signatures.v
- ZF.v
- Asimpl.v
- BinSig.v
- Bounded.v
- Core.v
- DiscreteEnumerable.v
- Facts.v
- Subst.v
- SyntacticOps.v
- Theories.v
- bpcp.v
- BPCP_SigBPCP.v
- btree.v
- decidable.v
- discernable.v
- discrete.v
- enumerable.v
- fo_congruence.v
- fo_definable.v
- fo_enum.v
- fo_logic.v
- fo_sat.v
- fo_sat_dec.v
- fo_sig.v
- fo_terms.v
- fol_ops.v
- gfp.v
- hfs.v
- membership.v
- notations.v
- red_chain_undec_full.v
- red_dec.v
- red_enum.v
- red_utils.v
- reln_hfs.v
- Sig0.v
- Sig1.v
- Sig1_1.v
- Sig2_Sign.v
- Sig2_SigSSn1.v
- Sig_discernable.v
- Sig_discrete.v
- Sig_no_syms.v
- Sig_noeq.v
- Sig_one_rel.v
- Sig_rem_constants.v
- Sig_rem_cst.v
- Sig_rem_props.v
- Sig_rem_syms.v
- Sig_Sig_fin.v
- Sig_uniform.v
- Sign1_Sig.v
- Sign_Sig.v
- Sign_Sig2.v
- utils.v
- FragmentSyntax.v
- FriedmanTranslation.v
- FriedmanTranslationFragment.v
- FullSyntax.v
- binFOL.v
- binFOL_undec.v
- binFST_undec.v
- binZF.v
- binZF_undec.v
- FOL.v
- FOL_undec.v
- FSAT.v
- FSAT_direct_undec.v
- FSAT_undec.v
- FST.v
- FST_undec.v
- minFOL_undec.v
- minZF.v
- minZF_undec.v
- PA.v
- PA_undec.v
- ZF.v
- ZF_undec.v
- Halt_REV_FRACTRAN_dec.v
- fractran_utils.v
- mm_fractran.v
- HaltTM_1_to_FRACTRAN_HALTING.v
- MM_computable_to_FRACTRAN_computable.v
- MM_FRACTRAN.v
- FRACTRAN_computable.v
- FRACTRAN_sss.v
- prime_seq.v
- FRACTRAN.v
- FRACTRAN_dec.v
- FRACTRAN_undec.v
- lagrange.v
- luca.v
- matrix.v
- Zp.v
- dio_binary.v
- dio_bounded.v
- dio_cipher.v
- dio_elem.v
- dio_expo.v
- dio_logic.v
- dio_rt_closure.v
- dio_single.v
- fractran_dio.v
- alpha.v
- cipher.v
- expo_diophantine.v
- FRACTRAN_computable_to_Diophantine.v
- H10_to_H10p.v
- Diophantine.v
- DPRM.v
- FRACTRAN_DIO.v
- H10.v
- H10_undec.v
- H10p.v
- H10p_undec.v
- H10Z.v
- H10Z_undec.v
- MPCPb_to_HSC_AX.v
- MPCPb_to_HSC_PRV.v
- HSCFacts.v
- HSC.v
- HSC_undec.v
- calculus.v
- confluence.v
- equivalence.v
- evaluator.v
- normalisation.v
- order.v
- prelim.v
- semantics.v
- syntax.v
- terms.v
- terms_extension.v
- typing.v
- conservativity.v
- conservativity_consequences.v
- conservativity_constants.v
- constants.v
- constants_consequences.v
- encoding.v
- reduction.v
- encoding.v
- motivation.v
- multiplication.v
- reduction.v
- diophantine_equations.v
- basic.v
- confluence.v
- evaluator.v
- list_reduction.v
- normalisation.v
- advanced.v
- basics.v
- misc.v
- countability.v
- decidable.v
- misc.v
- reductions.v
- retracts.v
- std.v
- tactics.v
- encoding.v
- huet.v
- pcp.v
- simplified.v
- higher_order_unification.v
- nth_order_unification.v
- systemunification.v
- unification.v
- axioms.v
- firstorder.v
- unscoped.v
- eill.v
- eill_mm.v
- ill.v
- ill_cll.v
- ill_cll_restr.v
- imsell.v
- schellinx.v
- EILL_CLL.v
- EILL_ILL.v
- iBPCP_MM.v
- ILL_CLL.v
- MM_EILL.v
- ndMM2_IMSELL.v
- CLL.v
- CLL_undec.v
- EILL.v
- ILL.v
- ILL_undec.v
- IMSELL.v
- IMSELL_undec.v
- CD_TYP_to_CD_TC.v
- SNclosed_to_CD_TYP.v
- SSTS01_to_CD_INH.v
- CD_facts.v
- CD_fundamental.v
- CD_sn.v
- CD_wn.v
- CD.v
- CD_undec.v
- wCBV.v
- Acceptability.v
- Computability.v
- Decidability.v
- Fixpoints.v
- MuRec.v
- Por.v
- Rice.v
- Scott.v
- Seval.v
- Synthetic.v
- List_basics.v
- List_enc.v
- List_eqb.v
- List_extra.v
- List_in.v
- List_nat.v
- LBool.v
- LFinType.v
- Lists.v
- LNat.v
- LOptions.v
- LProd.v
- LSum.v
- LTerm.v
- LUnit.v
- LVector.v
- HaltL_enum.v
- term_enum.v
- Ackermann.v
- Encoding.v
- EqBool.v
- Equality.v
- Eval.v
- FinTypeLookup.v
- Proc.v
- Subst.v
- ARS.v
- MuRec_extract.v
- H10_to_L.v
- HaltMuRec_to_HaltL.v
- MMA_computable_to_L_computable_closed.v
- MMA_HALTING_to_HaltLclosed.v
- MuRec_computable_to_L_computable.v
- PCPb_to_HaltL.v
- TM_to_L.v
- Computable.v
- ComputableTactics.v
- Extract.v
- GenEncode.v
- Lbeta.v
- Lbeta_nonrefl.v
- LClos.v
- Lproc.v
- Lrewrite.v
- Lsimpl.v
- LTactics.v
- Reflection.v
- TMinL_extract.v
- TapeFuns.v
- TMEncoding.v
- TMinL.v
- ClosedLAdmissible.v
- L_facts.v
- NaryApp.v
- term_facts.v
- L.v
- L_enum.v
- L_undec.v
- HaltLclosed_to_wCBNclosed.v
- KrivineMclosed_HALT_to_SNclosed.v
- SSTS01_to_HOMbeta.v
- wCBNclosed_to_KrivineMclosed_HALT.v
- confluence.v
- facts.v
- Krivine_facts.v
- stlc_facts.v
- term_facts.v
- wCBN_facts.v
- HOMatching.v
- HOMatching_undec.v
- Krivine.v
- Krivine_undec.v
- Lambda.v
- Lambda_undec.v
- acm2_utils.v
- MM2_REV_dec.v
- MM2_REV_HALT_dec.v
- MM2_UBOUNDED_dec.v
- MM2_UMORTAL_dec.v
- MM_2_HALTING_dec.v
- MPM2_HALT_dec.v
- mm_comp.v
- mm_comp_strong.v
- mm_defs.v
- mm_no_self.v
- mm_utils.v
- bsm_mma.v
- fractran_mma.v
- mma3_mma2_compiler.v
- mma_defs.v
- mma_k_mma_2_compiler.v
- mma_simul.v
- mma_utils.v
- mma_utils_bsm.v
- env.v
- mme_defs.v
- mme_utils.v
- ndmm2_utils.v
- BSM_computable_to_MM_computable.v
- BSM_HALTING_to_MM2_HALTING.v
- BSM_MM.v
- BSM_to_MMA_HALTING.v
- FRACTRAN_to_MMA2.v
- HaltTM_1_to_MM.v
- KrivineMclosed_HALT_to_MMA_HALTING.v
- L_computable_closed_to_MMA_computable.v
- MM2_HALTING_to_MM2_ZERO_HALTING.v
- MM2_to_ndMM2_ACCEPT.v
- MM_computable_to_MMA_computable.v
- MM_to_MMA2.v
- MMA2_to_MM2.v
- MMA2_to_MMA2_zero.v
- MMA2_to_ndMM2_ACCEPT.v
- MMA3_to_MMA2_HALTING.v
- MMA_computable_to_MMA_mon_computable.v
- MuRec_computable_to_MM_computable.v
- MUREC_MM.v
- ndMM2_to_ACM2_ACCEPT.v
- PCPb_to_MM.v
- SBTM_to_MMA2_HALTING.v
- MM2_facts.v
- MM_computable.v
- MM_sss.v
- MMA_computable.v
- MMA_facts.v
- MMA_pairing.v
- ACM2.v
- ACM2_undec.v
- MM.v
- MM2.v
- MM2_dec.v
- MM2_undec.v
- MM_dec.v
- MM_undec.v
- MMA.v
- MMA2_undec.v
- ndMM2.v
- ndMM2_undec.v
- Diophantine_to_MuRec_computable.v
- H10_to_MUREC_HALTING.v
- H10C_SAT_to_RA_UNIV_HALT.v
- beta.v
- enumerable.v
- eval.v
- minimizer.v
- MuRec_computable.v
- prim_min.v
- ra_ca.v
- ra_dio_poly.v
- ra_enum.v
- ra_godel_beta.v
- ra_mm.v
- ra_mm_env.v
- ra_recomp.v
- ra_sem_eq.v
- ra_simul.v
- ra_univ.v
- ra_univ_andrej.v
- RA_UNIV_HALT.v
- RA_UNIV_HALT_undec.v
- ra_utils.v
- recalg.v
- recomp.v
- recursor.v
- MuRec.v
- MuRec_undec.v
- HaltTM_1_to_iPCPb.v
- HaltTM_1_to_PCP.v
- HaltTM_1_to_PCPb.v
- MPCP_to_MPCPb.v
- MPCP_to_PCP.v
- PCP_to_PCPb.v
- PCPb_iff_BPCP.v
- PCPb_iff_dPCPb.v
- PCPb_iff_iPCPb.v
- PCPX_iff_dPCP.v
- SR_to_MPCP.v
- Facts.v
- PCP_facts.v
- LICENSE
- PCP.v
- PCP_undec.v
- FMsetC_SAT_to_LPolyNC_SAT.v
- LPolyNC.v
- LPolyNC_undec.v
- CSSM_UB_to_SSemiU.v
- HaltTM_1_chain_SemiU.v
- HaltTM_1_to_SemiU.v
- RU2SemiU_to_LU2SemiU.v
- RU2SemiU_to_SemiU.v
- SSemiU_to_RU2SemiU.v
- Enumerable.v
- SemiU.v
- SemiU_undec.v
- FSATdc_to_MSLSAT.v
- MSLSAT_to_SLSAT.v
- MSL.v
- MSL_undec.v
- SL.v
- SL_undec.v
- H10UC_SAT_to_FMsetC_SAT.v
- Facts.v
- FMsetC.v
- FMsetC_undec.v
- compiler.v
- compiler_correction.v
- sss.v
- subcode.v
- binomial.v
- bool_list.v
- bool_nat.v
- bounded_quantification.v
- crt.v
- fin_base.v
- fin_bij.v
- fin_choice.v
- fin_dec.v
- fin_quotient.v
- fin_upto.v
- finite.v
- focus.v
- gcd.v
- godel_coding.v
- interval.v
- list_bool.v
- list_focus.v
- php.v
- power_decomp.v
- prime.v
- quotient.v
- rel_iter.v
- seteq.v
- sorting.v
- sums.v
- utils.v
- utils_decidable.v
- utils_list.v
- utils_nat.v
- utils_string.v
- utils_tac.v
- pos.v
- vec.v
- acc_irr.v
- measure_ind.v
- wf_chains.v
- wf_finite.v
- wf_incl.v
- BasicDefinitions.v
- BasicFinTypes.v
- CompoundFinTypes.v
- DepPairs.v
- FinTypes.v
- FinTypesDef.v
- VectorFin.v
- BaseLists.v
- Tactics.v
- FinNotation.v
- Vectors.v
- Base.v
- EqDec.v
- EqDecDef.v
- FiniteTypes.v
- Inhabited.v
- Numbers.v
- Prelim.v
- Dec.v
- ListAutomation.v
- simulation.v
- H10p_to_SOL.v
- PA2_categoricity.v
- PA2_facts.v
- Subst.v
- Syntax.v
- Tarski.v
- PA2.v
- PA2_undec.v
- SOL.v
- SOL_undec.v
- bsm_defs.v
- bsm_pcp.v
- bsm_pctm.v
- bsm_utils.v
- tiles_solvable.v
- CM1_to_SMX.v
- SMX.v
- SMX_facts.v
- CM1_HALT_to_SMNdl_UB.v
- HaltTM_1_to_CSSM_UB.v
- iPCPb_to_BSM_HALTING.v
- PCTM_HALT_to_BSM_HALTING.v
- SBTM_HALT_to_HaltBSM.v
- SMNdl_UB_to_CSSM_UB.v
- TM_computable_to_BSM_computable.v
- BSM_computable.v
- BSM_sss.v
- CSSM_facts.v
- Enumerable.v
- List_facts.v
- Nat_facts.v
- SMN_facts.v
- SMN_transform.v
- BSM.v
- BSM_undec.v
- SMN.v
- SMN_undec.v
- SSM.v
- SSM_undec.v
- HaltTM_1_to_SR.v
- MM2_ZERO_HALTING_to_SSTS01.v
- SBTM_HALT_to_SR.v
- SBTM_HALT_to_TSR.v
- SR_to_PCSnf.v
- Definitions.v
- PCSnf.v
- PCSnf_undec.v
- SR.v
- SR_undec.v
- SSTS.v
- SSTS_undec.v
- DecidabilityFacts.v
- Definitions.v
- EnumerabilityFacts.v
- Infinite.v
- InformativeDefinitions.v
- InformativeReducibilityFacts.v
- ListEnumerabilityFacts.v
- Models_Equivalent.v
- MoreEnumerabilityFacts.v
- MoreReducibilityFacts.v
- ReducibilityFacts.v
- SemiDecidabilityFacts.v
- Undecidability.v
- syntax.v
- sysf.sig
- unscoped.v
- H10C_SAT_to_SysF_INH.v
- HaltTM_1_to_SysF_INH.v
- HaltTM_1_to_SysF_TC.v
- HaltTM_1_to_SysF_TYP.v
- LU2SemiU_to_SysF_TYP.v
- SysF_TYP_to_SysF_TC.v
- Facts.v
- iipc2_facts.v
- poly_type_facts.v
- pure_term_facts.v
- pure_typable_prenex.v
- pure_typing_facts.v
- sn_facts.v
- step.v
- term_facts.v
- typing_facts.v
- SysF.v
- SysF_undec.v
- Mono.v
- Code.v
- Combinators.v
- If.v
- Mirror.v
- SequentialComposition.v
- StateWhile.v
- Switch.v
- While.v
- MoveToSymbol.v
- Multi.v
- Shift.v
- TMTac.v
- WriteString.v
- SBTM_HALT_enum.v
- pctm_defs.v
- pctm_sbtm.v
- Arbitrary_to_Binary.v
- HaltLclosed_to_HaltTM_5.v
- HaltTM_1_to_SBTM_HALT.v
- KrivineMclosed_HALT_to_HaltUTM.v
- MMA_computable_to_TM_computable.v
- MMA_HALTING_n_to_HaltTM_n.v
- MMA_mon_computable_to_TM_computable.v
- mTM_to_TM.v
- SBTM_HALT_to_HaltTM_1.v
- SBTM_HALT_to_PCTM_HALT.v
- EncodeTapes.v
- StepTM.v
- Prelim.v
- Relations.v
- SBTM_facts.v
- TM_computable.v
- TM_facts.v
- PCTM.v
- SBTM.v
- SBTM_enum.v
- SBTM_undec.v
- TM.v
- TM_undec.v
- UTM.v
- UTM_undec.v
- .gitignore
- _CoqProject
- Makefile
- footer.html
- header.html
- .gitignore
- config.js
- coqdoc.css
- coqdocjs.css
- coqdocjs.js
- .gitignore
- .gitmodules
- LICENSE
- Makefile
- opam
- README.md
// repository documentation
Was this content helpful?
(0 ratings)