Difference between revisions of "Formal system"
From apm
(loads of Wikipedia links - roughly grouped) |
(formatting for better readability) |
||
| (4 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{stub}} | {{stub}} | ||
| − | |||
| − | |||
| − | |||
== External links == | == External links == | ||
| − | * Experiencing systems as a puzzle game - very good! http://incredible.pm/ | + | * Experiencing formal systems as a puzzle game - very good! <br> '''The Incredible Proof Machine http://incredible.pm/''' |
=== Wikipedia === | === Wikipedia === | ||
* [https://en.wikipedia.org/wiki/Formal_system Formal_system], [https://en.wikipedia.org/wiki/Formal_language Formal_language], [https://en.wikipedia.org/wiki/Formal_grammar Formal_grammar] ([https://en.wikipedia.org/wiki/Abstract_syntax_tree Abstract_syntax_tree], [https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form Backus–Naur_form]) | * [https://en.wikipedia.org/wiki/Formal_system Formal_system], [https://en.wikipedia.org/wiki/Formal_language Formal_language], [https://en.wikipedia.org/wiki/Formal_grammar Formal_grammar] ([https://en.wikipedia.org/wiki/Abstract_syntax_tree Abstract_syntax_tree], [https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form Backus–Naur_form]) | ||
| − | * [https://en.wikipedia.org/wiki/Rewriting Rewriting] and [https://en.wikipedia.org/wiki/Substitution_(logic) Substitution] | + | * [https://en.wikipedia.org/wiki/Rewriting Rewriting] and [https://en.wikipedia.org/wiki/Substitution_(logic) Substitution], [https://en.wikipedia.org/wiki/Explicit_substitution Explicit_substitution] |
* [https://en.wikipedia.org/wiki/Chomsky_hierarchy Chomsky_hierarchy] | * [https://en.wikipedia.org/wiki/Chomsky_hierarchy Chomsky_hierarchy] | ||
---- | ---- | ||
| − | * [https://en.wikipedia.org/wiki/Boolean_algebra Boolean_algebra] ([https://en.wikipedia.org/wiki/De_Morgan%27s_laws De Morgan's laws]) | + | * [https://en.wikipedia.org/wiki/Boolean_algebra Boolean_algebra] ([https://en.wikipedia.org/wiki/De_Morgan%27s_laws De Morgan's laws], [https://en.wikipedia.org/wiki/Karnaugh_map Karnaugh_map]) |
* [https://en.wikipedia.org/wiki/Propositional_calculus Propositional_calculus], [https://en.wikipedia.org/wiki/Second-order_propositional_logic Second-order_propositional_logic] ([https://en.wikipedia.org/wiki/Second-order_logic Second-order_logic]), [https://en.wikipedia.org/wiki/Higher-order_logic Higher-order_logic] | * [https://en.wikipedia.org/wiki/Propositional_calculus Propositional_calculus], [https://en.wikipedia.org/wiki/Second-order_propositional_logic Second-order_propositional_logic] ([https://en.wikipedia.org/wiki/Second-order_logic Second-order_logic]), [https://en.wikipedia.org/wiki/Higher-order_logic Higher-order_logic] | ||
---- | ---- | ||
* [https://en.wikipedia.org/wiki/Intuitionistic_logic Intuitionistic_logic], [https://en.wikipedia.org/wiki/Intuitionistic_type_theory Intuitionistic_type_theory], [https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence Curry–Howard_correspondence] | * [https://en.wikipedia.org/wiki/Intuitionistic_logic Intuitionistic_logic], [https://en.wikipedia.org/wiki/Intuitionistic_type_theory Intuitionistic_type_theory], [https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence Curry–Howard_correspondence] | ||
| − | * [https://en.wikipedia.org/wiki/Lambda_calculus | + | * [https://en.wikipedia.org/wiki/Lambda_calculus Untyped_lambda_calculus], [https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus Simply_typed_lambda_calculus], [https://en.wikipedia.org/wiki/Typed_lambda_calculus Typed_lambda_calculus], [https://en.wikipedia.org/wiki/System_F System_F] |
| − | * [https://en.wikipedia.org/wiki/Evaluation_strategy Evaluation_strategy] | + | * [https://en.wikipedia.org/wiki/Evaluation_strategy Evaluation_strategy], [https://en.wikipedia.org/wiki/De_Bruijn_index De_Bruijn_index] (or better [https://pchiusano.github.io/2014-06-20/simple-debruijn-alternative.html alternative]) |
| + | * [https://en.wikipedia.org/wiki/Lambda_cube Lambda_cube], [https://en.wikipedia.org/wiki/Dependent_type Dependent_type] | ||
---- | ---- | ||
| − | * [https://en.wikipedia.org/wiki/Foundations_of_mathematics Foundations_of_mathematics], [https://en.wikipedia.org/wiki/Category_theory Category_theory] | + | * [https://en.wikipedia.org/wiki/Foundations_of_mathematics Foundations_of_mathematics], [https://en.wikipedia.org/wiki/Category_theory Category_theory], [https://en.wikipedia.org/wiki/Corecursion Corecursion] |
* [https://en.wikipedia.org/wiki/Categorical_logic Categorical_logic] [https://en.wikipedia.org/wiki/Cartesian_closed_category Bicartesian_closed_category] (Homotopy type theory, Lawvere theories) | * [https://en.wikipedia.org/wiki/Categorical_logic Categorical_logic] [https://en.wikipedia.org/wiki/Cartesian_closed_category Bicartesian_closed_category] (Homotopy type theory, Lawvere theories) | ||
---- | ---- | ||
| Line 27: | Line 25: | ||
[[Category:Information]] | [[Category:Information]] | ||
| + | [[Category:Programming]] | ||
Latest revision as of 10:50, 26 September 2021
External links
- Experiencing formal systems as a puzzle game - very good!
The Incredible Proof Machine http://incredible.pm/
Wikipedia
- Formal_system, Formal_language, Formal_grammar (Abstract_syntax_tree, Backus–Naur_form)
- Rewriting and Substitution, Explicit_substitution
- Chomsky_hierarchy
- Boolean_algebra (De Morgan's laws, Karnaugh_map)
- Propositional_calculus, Second-order_propositional_logic (Second-order_logic), Higher-order_logic
- Intuitionistic_logic, Intuitionistic_type_theory, Curry–Howard_correspondence
- Untyped_lambda_calculus, Simply_typed_lambda_calculus, Typed_lambda_calculus, System_F
- Evaluation_strategy, De_Bruijn_index (or better alternative)
- Lambda_cube, Dependent_type
- Foundations_of_mathematics, Category_theory, Corecursion
- Categorical_logic Bicartesian_closed_category (Homotopy type theory, Lawvere theories)
