stanford-oval/wikipedia huggingface dataset:
Pelecopsis minor

| Pelecopsis minor> Phân loại khoa học |
| --- | --- |
Giới (regnum): Animalia
Ngành (phylum): Arthropoda
Phân ngành (subphylum): Chelicerata
(không phân hạng): Arachnomorpha
Lớp (class): Arachnida
Bộ (ordo): Araneae
Họ (familia): Linyphiidae
Chi (genus): Pelecopsis
Loài (species): P. minor
Danh pháp hai phần
Pelecopsis minor Wunderlich, 1995 
Pelecopsis minor là một loài nhện trong họ Linyphiidae.
Loài này thuộc chi Pelecopsis. Pelecopsis minor được Jörg Wunderlich miêu tả năm 1995.
Chú thích

↑  Platnick, Norman I. (2010): The world spider catalog, version 10.5. American Museum of Natural History.
Cheilanthes tenuissima

| Cheilanthes tenuissima> Phân loại khoa học |
| --- | --- |
Giới (regnum): Plantae
Ngành (divisio): Pteridophyta
Lớp (class): Polypodiopsida
Bộ (ordo): Polypodiales
Họ (familia): Pteridaceae
Chi (genus): Cheilanthes
Loài (species): C. tenuissima
Danh pháp hai phần
Cheilanthes tenuissima Bailey, 1906 
Cheilanthes tenuissima là một loài dương xỉ trong họ Pteridaceae. Loài này được Bailey mô tả khoa học đầu tiên năm 1906.
Danh pháp khoa học của loài này chưa được làm sáng tỏ.
Chú thích

↑  The Plant List (2010). “Cheilanthes tenuissima”. Truy cập ngày 28 tháng 5 năm 2014.
Prunus herthae

| Prunus herthae> Tình trạng bảo tồn |
| --- | --- |
 Thiếu dữ liệu  (IUCN 3.1)
Phân loại khoa học
Giới (regnum): Plantae
(không phân hạng): Angiospermae
(không phân hạng): Eudicots
(không phân hạng): Rosids
Bộ (ordo): Rosales
Họ (familia): Rosaceae
Chi (genus): Prunus
Loài (species): P. herthae
Danh pháp hai phần
Prunus herthae Diels 
Prunus herthae là loài thực vật có hoa trong họ Hoa hồng. Loài này được Diels miêu tả khoa học đầu tiên năm 1941.
Chú thích

↑  The Plant List (2010). “Prunus herthae”. Truy cập ngày 11 tháng 6 năm 2013.[liên kết hỏng]
Vitex doniana

| Vitex doniana |
| --- | --- |

Phân loại khoa học
Giới (regnum): Plantae
(không phân hạng): Angiospermae
(không phân hạng): Eudicots
Bộ (ordo): Lamiales
Họ (familia): Lamiaceae
Chi (genus): Vitex
Loài (species): V. doniana
Danh pháp hai phần
Vitex doniana Sweet, 1826 
Vitex doniana là một loài thực vật có hoa trong họ Hoa môi. Loài này được Sweet miêu tả khoa học đầu tiên năm 1826.
Chú thích

↑  The Plant List (2010). “Vitex doniana”. Truy cập ngày 5 tháng 6 năm 2013.
Kafr Safra

| Kafar safra كفر صفرة كفر صفرة |
| --- | --- |
—  Town  —
Kafr Safra
 
Kafar safra كفر صفرة
Country:  Syria
Governorate: Aleppo Governorate
District: Afrin District
Subdistrict: Jindires
Thủ phủ:  FSA Turks control
Control:  Turkish-backed  Free Syrian Army
Chính quyền
 • Kiểu: Coat of arms of North Korea.svg
 • Captured area Bản mẫu:Country data Syrian Opposition: Haji Abdo is terrorist
Diện tích
 • Tổng cộng: 50 km2 (20 mi2)
 • Mặt nước: 26 km2 (10 mi2)  38%
Dân số (2019 census)
 • Tổng cộng: 2,230
 : Kurds Most of them
Múi giờ: EET (UTC+2)
 • Mùa hè (DST): EEST (UTC+3)
Kafr Safra (tiếng Ả Rập: كفر صفرة‎, cũng đánh vần là Kafar Safra) là một ngôi làng ở miền bắc Syria, một phần hành chính của quận Afrin của Tỉnh Aleppo, nằm ở phía tây bắc Aleppo. Các địa phương gần đó bao gồm Sheikh al-Hadid ở phía bắc, Qarah Bash ở phía đông và Jindires ở phía nam. Theo Cục Thống kê Trung ương Syria (CBS), Kafr Safra có dân số 2.150 trong cuộc điều tra dân số năm 2004. Kafr Safra đã nằm dưới sự kiểm soát của YPG kể từ tháng 8 năm 2012. Thị trấn cuối cùng đã nằm dưới sự kiểm soát của Quân đội Syria Tự do do Thổ Nhĩ Kỳ hậu thuẫn vào ngày 9 tháng 3 năm 2018.
Unoprostone

| --- | --- |

Dữ liệu lâm sàng
Tên thương mại: Rescula
AHFS/Drugs.com: Thông tin tiêu dùng chi tiết Micromedex
Danh mục cho thai kỳ:  US: C (Rủi ro không bị loại trừ)   
Dược đồ sử dụng: Topical (eye drops)
Mã ATC: S01EE02 (WHO) 
Tình trạng pháp lý
Tình trạng pháp lý:  US: Discontinued  
Dữ liệu dược động học
Chu kỳ bán rã sinh học: 14 min
Bài tiết: Thận
Các định danh
 Tên IUPAC (Z)-7-[(1R,2R,3R,5S)-3,5-dihydroxy-2-(3-oxodecyl) cyclopentyl]hept-5-enoic acid 
Số đăng ký CAS: 120373-36-6 120373-24-2  (isopropyl ester)
PubChem CID: 5311236
DrugBank: DB06826 N
ChemSpider: 4470755 N
Định danh thành phần duy nhất: 6X4F561V3W
KEGG: D08661 Y
ChEMBL: CHEMBL1201407 N
ECHA InfoCard: 100.227.145
Dữ liệu hóa lý
Công thức hóa học: C22H38O5
Khối lượng phân tử: 382.534 g/mol
Mẫu 3D (Jmol): Hình ảnh tương tác
 SMILES O=C(O)CCC/C=C\C[C@H]1[C@@H](O)C[C@@H](O)[C@@H]1CCC(=O)CCCCCCC 
 Định danh hóa học quốc tế InChI=1S/C22H38O5/c1-2-3-4-5-8-11-17(23)14-15-19-18(20(24)16-21(19)25)12-9-6-7-10-13-22(26)27/h6,9,18-21,24-25H,2-5,7-8,10-16H2,1H3,(H,26,27)/b9-6-/t18-,19-,20+,21-/m1/s1 N Key:TVHAZVBUYQMHBC-SNHXEXRGSA-N N 
  (kiểm chứng)
Unoprostone (INN) là một chất tương tự tuyến tiền liệt. Este isopropyl của nó, unoprostone isopropyl, đã được bán trên thị trường dưới tên thương mại Rescula để điều trị bệnh tăng nhãn áp góc mở, nhưng hiện đã ngừng ở Mỹ.
Cheilanthes thellungii

| Cheilanthes thellungii> Phân loại khoa học |
| --- | --- |
Giới (regnum): Plantae
Ngành (divisio): Pteridophyta
Lớp (class): Polypodiopsida
Bộ (ordo): Polypodiales
Họ (familia): Pteridaceae
Chi (genus): Cheilanthes
Loài (species): C. thellungii
Danh pháp hai phần
Cheilanthes thellungii Herter, 1925 
Cheilanthes thellungii là một loài dương xỉ trong họ Pteridaceae. Loài này được Herter mô tả khoa học đầu tiên năm 1925.
Danh pháp khoa học của loài này chưa được làm sáng tỏ.
Chú thích

↑  The Plant List (2010). “Cheilanthes thellungii”. Truy cập ngày 28 tháng 5 năm 2014.
Pelecopsis mutica

| Pelecopsis mutica> Phân loại khoa học |
| --- | --- |
Giới (regnum): Animalia
Ngành (phylum): Arthropoda
Phân ngành (subphylum): Chelicerata
(không phân hạng): Arachnomorpha
Lớp (class): Arachnida
Bộ (ordo): Araneae
Họ (familia): Linyphiidae
Chi (genus): Pelecopsis
Loài (species): P. mutica
Danh pháp hai phần
Pelecopsis mutica J. Denis, 1957 
Pelecopsis mutica là một loài nhện trong họ Linyphiidae.
Loài này thuộc chi Pelecopsis. Pelecopsis mutica được J. Denis miêu tả năm 1957.
Chú thích

↑  Platnick, Norman I. (2010): The world spider catalog, version 10.5. American Museum of Natural History.
Phước Tân (định hướng)

Phước Tân có thể là:
Phường Phước Tân, thành phố Biên Hòa, tỉnh Đồng Nai
Xã Phước Tân, huyện Xuyên Mộc, tỉnh Bà Rịa – Vũng Tàu
Xã Phước Tân, huyện Phú Riềng, tỉnh Bình Phước
Xã Phước Tân, huyện Bác Ái, tỉnh Ninh Thuận
Xã Phước Tân, huyện Sơn Hòa, tỉnh Phú Yên
Phường cũ Phước Tân thuộc thành phố Nha Trang, tỉnh Khánh Hòa; nay là một phần của phường Tân Tiến.
Piliocolobus kirkii

| Procolobus kirkii |
| --- | --- |

Tình trạng bảo tồn
 Nguy cấp  (IUCN 3.1)
Phân loại khoa học
Giới (regnum): Animalia
Ngành (phylum): Chordata
Lớp (class): Mammalia
Bộ (ordo): Primates
Họ (familia): Cercopithecidae
Chi (genus): Procolobus
Phân chi (subgenus): Piliocolobus
Loài (species): P. kirkii
Danh pháp hai phần
Procolobus kirkii (Gray, 1868) 
 
Procolobus kirkii là một loài động vật có vú trong họ Cercopithecidae, bộ Linh trưởng. Loài này được Gray mô tả năm 1868.
Đây là loài loài đặc hữu của Unguja, hòn đảo chính của quần đảo Zanzibar, ngoài khơi bờ biển Tanzania.
Chú thích

↑  Struhsaker T & Siex K (2008). Procolobus kirkii. 2008 Sách đỏ IUCN. Liên minh Bảo tồn Thiên nhiên Quốc tế 2008. Truy cập ngày 4 tháng 1 năm 2009.
1 2  Wilson, D. E.; Reeder, D. M. biên tập (2005). “Piliocolobus kirkii”. Mammal Species of the World . Baltimore: Nhà in Đại học Johns Hopkins, 2 tập (2.142 trang). ISBN 978-0-8018-8221-0. OCLC 62265494.
Kafr al-Tun

| Kafr al-Tun كفر الطون Kfar Eltun |
| --- | --- |
—  Village  —
 
Kafr al-TunLocation in Syria
Country:  Syria
Governorate: Hama
District: Hama
Subdistrict: Hama
Dân số (2004)
 • Tổng cộng: 2,655
Kafr al-Tun (tiếng Ả Rập: كفر الطون‎, cũng đánh vần là Kfar Eltun) là một ngôi làng ở phía tây bắc Syria, một phần hành chính của Tỉnh Hama, phía tây Hama. Các địa phương gần đó bao gồm al-Majdal ở phía tây bắc, Khitab ở phía đông bắc, Shihat Hama ở phía đông, Tayzin ở phía đông nam và al-Rabiaa ở phía đông. Theo Cục Thống kê Trung ương, Kafr al-Tun có dân số 2.655 trong cuộc điều tra dân số năm 2004. Cư dân của nó chủ yếu là người Hồi giáo Sunni.
Juniperus ashei

| Juniperus ashei> Tình trạng bảo tồn |
| --- | --- |
 Ít quan tâm  (IUCN 3.1)
Phân loại khoa học
Giới (regnum): Plantae
(không phân hạng): Gymnospermae
Lớp (class): Pinopsida
Bộ (ordo): Pinales
Họ (familia): Cupressaceae
Chi (genus): Juniperus
Loài (species): J. ashei
Danh pháp hai phần
Juniperus ashei J.Buchholz, 1930 
Juniperus ashei là một loài thực vật hạt trần trong họ Cupressaceae. Loài này được J.Buchholz mô tả khoa học đầu tiên năm 1930.
Chú thích

↑  The Plant List (2010). “Juniperus ashei”. Truy cập ngày 28 tháng 5 năm 2014.
LXDE

| --- | --- |

Màn hình desktop mặc định của LXDE
Thiết kế bởi: Hong Jen Yee ("PCMan")
Phát triển bởi: Nhóm LXDE
Phát hành lần đầu: 2006; 18 năm trước (2006)

Phiên bản cuối: 0.99.2    / 22 tháng 11 năm 2016; 7 năm trước (2016-11-22)
 
Kho mã nguồn: github.com/lxde  
Viết bằng: C, GTK
Hệ điều hành: Tương tự Unix
Nền tảng: Linux, BSD
Ngôn ngữ có sẵn: 35 ngôn ngữ khác nhau
Thể loại: Môi trường desktop
Giấy phép: Giấy phép công cộng GNU (GPL) hoặc thương mại
Website: lxde.org
Trạng thái: Thay thế bởi LXQt
LXDE (viết tắt của Lightweight X11 Desktop Environment) là một môi trường desktop tự do nguồn mở cho các hệ thống UNIX và tương tự Unix tương thích với POSIX, với yêu cầu tài nguyên tương đối thấp. Điều này làm cho nó đặc biệt phù hợp để sử dụng trên máy tính cá nhân giống như netbook hay máy tính SoC. LXDE tiết kiệm năng lượng và chạy nhanh.. Có thể phát triển LXDE trên nhiều phiên bản khác nhau của Linux như Ubuntu hay Debian. Do vậy, những ứng dụng có thể chạy trên các hệ điều hành này sẽ hoạt động với LXDE. LXDE hiện đã đang hỗ trợ nhiều kiến trúc bộ vi xử lý trong đó có các kiến trúc của Intel hay MIPS. Nhóm phát triển LXDE cũng có kế hoạch chuyển môi trường desktop sang một kiến trúc phần cứng khác như ARM vốn thường được dùng trong các thiết bị nhúng như điện thoại di động.
Tổng quan

LXDE được viết bằng C, dùng bộ công cụ GTK+ 2, và chạy trên Unix và các hệ thống tương thích POSIX, ví như Linux và BSD. Dự án LXDE nhằm cung cấp một môi trường desktop nhanh và tiết kiệm năng lượng.
Năm 2010, các thử nghiệm cho thấy LXDE 0.5 có mức sử dụng bộ nhớ thấp nhất trong bốn môi trường máy tính để bàn phổ biến nhất thời bấy giờ (các môi trường khác là GNOME 2.29, KDE Plasma Desktop 4.4, và Xfce 4.6), và nó tiêu thụ ít năng lượng hơn, điều này cho thấy máy tính di động với các bản phân phối Linux chạy LXDE 0.5 đã làm hết pin của chúng với tốc độ chậm hơn so với các bản phân phối có môi trường máy tính để bàn khác.
LXDE là môi trường desktop mặc định của Knoppix, LXLE Linux, và Peppermint Linux OS - và một số các bản phân phối khác. Trong nhiều năm, nó là desktop cho Lubuntu cho đến khi bị thay thế bởi LXQt năm 2018. Ngoài ra, desktop PIXEL của Raspbian (hệ điều hành chính thức của Raspberry Pi) là phiên bản sửa đổi cao của LXDE.
LXDE sử dụng các bản phát hành rolling releases cho các thành phần riêng lẻ của nó (hoặc cho các nhóm thành phần có phụ thuộc được ghép nối). Trình quản lý của sổ mặc định là Openbox, nhưng người ta có thể định cấu hình trình quản lý cửa sổ của bên thứ ba để sử dụng với LXDE, ví dụ như Fluxbox, IceWM hay Xfwm.
LXDE bao gồm mã được cấp phép GPL cũng như mã được cấp phép LGPL.
Lịch sử

Dự án được bắt đầu năm 2006 lập trình viên người Đài Loan Hong Jen Yee (tiếng Trung: 洪任諭; bính âm: Hóng Rènyù), còn gọi là PCMan, khi ông phát hành PCManFM, một trình quản lý file mới và mô-đun đầu tiên của LXDE.
So sánh bảng xếp hạng phân phối của DistroWatch vào đầu tháng 1 năm 2011 cho năm 2010 so với năm 2009, Ladislav Bodnar lưu ý sự gia tăng mức độ phổ biến của LXDE so với các môi trường máy tính để bàn khác. Ông nói:
Nhìn qua các bảng, một điều thú vị là sự gia tăng của các bản phân phối sử dụng máy tính để bàn LXDE nhẹ, nhưng đầy đủ tính năng hoặc trình quản lý cửa sổ Openbox. Ví dụ, giờ đây, Lubuntu thoải mái đánh bại Kubuntu về lượt truy cập trang, trong khi CrunchBang Linux, một bản phân phối nhẹ với Openbox vẫn nằm trong top 25 mặc dù nó không tạo được bản phát hành ổn định trong hơn một năm. Nhiều bản phân phối khác bắt đầu cung cấp các phiên bản dựa trên LXDE cho các sản phẩm của họ, góp phần tăng thêm sự phổ biến của môi trường desktop tương đối mới này.
Lịch sử > Qt port

Bài chi tiết: LXQt
Không hài lòng với GTK+ 3, Hong Jen Yee đã thử nghiệm với Qt đầu năm 2013 và phát hành phiên bản đầu tiên của PCManFM dựa trên Qt ngày 26 tháng 3, 2013.
Ngày 3 tháng 7, 2013 Hong đã công bố một port Qt đầy đủ của cả bộ LXDE, và vào ngày 21 tháng 7 Razor-qt và LXDE thông báo rằng họ sẽ hợp nhất hai dự án. Việc sáp nhập này có nghĩa là phiên bản GTK+ và Qt sẽ cùng tồn tại trong một thời gian nhưng cuối cùng, phiên bản GTK sẽ bị loại bỏ và mọi nỗ lực tập trung vào port Qt.
Các phần mềm thành phần của LXDE

Không giống như các môi trường desktop lớn khác như GNOME, các thành phần của LXDE có ít phụ thuộc và không được tích hợp chặt chẽ. Thay vào đó, chúng có thể được cài đặt độc lập với nhau hoặc với chính LXDE.
| Thành phần | Mô tả | Ghi chú |
| --- | --- | --- |
| PCMan File Manager | Trình quản lý file |  |
| LXInput | Công cụ cấu hình chuột và bàn phím |  |
| LXLauncher | Trình khởi chạy ứng dụng chế độ dễ dàng |  |
| LXPanel | Desktop panel |  |
| LXSession | X session manager |  |
| LXAppearance | Chuyển đổi giữa các theme GTK+ |  |
| GPicView | Trình xem ảnh |  |
| LXMusic | Một frontend cho trình đa phương tiện XMMS2 |  |
| LXTerminal | Giả lập Terminal | LXTerminal có thể được cấu hình để ẩn thanh menu và thanh cuộn |
| LXTask | Task manager |  |
| LXRandR | Một GUI cho RandR |  |
| LXDM | X display manager |  |
| LXNM | Lightweight network connection helper daemon. Supports wireless connections (Linux only). | Ngừng phát triển |
| Leafpad | Trình soạn thảo văn bản | Không được phát triển bởi dự án LXDE |
| Openbox (Fluxbox, IceWM and Xfwm are also supported) | Trình quản lý cửa sổ | Không được phát triển bởi dự án LXDE |
| ObConf | Một công cụ GUI để cấu hình Openbox | Không được phát triển bởi dự án LXDE |
| Xarchiver | Nén và lưu trữ dữ liệu | Không được phát triển bởi dự án LXDE |
Các phần mềm thành phần của LXDE > Phần mềm

Phần lớn các ứng dụng dành cho LXDE bao gồm các phần mềm mã nguồn mở, miễn phí và tự do. Ngoài ra cũng có một số ít các phần mềm thương mại chạy trên LXDE.
OpenOffice.org
Skype
Firefox
Thunderbird
Pidgin
Synaptic
Audacity
SMPlayer
LXDE Screenshots

LXDE Picture Viewer
LXappearance
LXpanel
LXpanel Preferences
PCManFM
PCManFM
GPicView
LXAppearance
LXTask
Autocompletion of Panel tasks
Màn hình desktop LXDE trên Arch Linux
TVP Dokument

| --- | --- |

Quốc gia: Ba Lan
Trụ sở: Warszawa
Chương trình
Ngôn ngữ: Tiếng Ba Lan
Định dạng hình: 16:9 HDTV
Sở hữu
Chủ sở hữu: Đài Truyền hình Ba Lan
Lịch sử
Lên sóng: 19 tháng 11 năm 2020; 3 năm trước (2020-11-19)
Liên kết ngoài
Website: dokument.tvp.pl
TVP Dokument là kênh truyền hình của Ba Lan, các chương trình chủ yếu về phim tài liệu và phim điện ảnh. Kênh bắt đầu được phát sóng vào ngày 19 tháng 11 năm 2020. Kênh chỉ được phát ở định dạng HD qua cáp và vệ tinh, cũng như truyền thử nghiệm DVB-T2/HEVC.
Suy luận tự động

Ngành nhỏ của khoa học máy tính và logic họcBản mẫu:SHORTDESC:Ngành nhỏ của khoa học máy tính và logic học
Trong khoa học máy tính, đặc biệt là trong biểu diễn tri thức và siêu logic học, lĩnh vực suy luận tự động (automated reasoning) được dành riêng cho việc hiểu các khía cạnh khác nhau của lý trí. Nghiên cứu về suy luận tự động giúp phát triển các chương trình máy tính cho phép máy tính suy luận hoàn toàn, hoặc gần như hoàn toàn tự động. Mặc dù suy luận tự động được coi là một phân ngành của trí tuệ nhân tạo, nó cũng có sự liên kết với khoa học máy tính lý thuyết và triết học.
Các phân ngành phát triển mạnh nhất của suy luận tự động là "chứng minh định lý tự động" hay "automated theorem proving" (và phân ngành kém tự động hơn nhưng thực tế hơn là "chứng minh định lý tương tác" hay "interactive theorem proving") và "kiểm tra chứng minh tự động" hay "automated proof checking" (được coi là suy luận chính xác đảm bảo theo các giả định cố định). Rất nhiều công trình cũng đã được thực hiện trong suy luận theo loại suy bằng cách sử dụng quy nạp và giả định.
Các chủ đề quan trọng khác bao gồm suy luận trong điều kiện bất định và suy luận phi đơn điệu. Một phần quan trọng của lĩnh vực bất định là lập luận, nơi các ràng buộc về tối thiểu hóa và tính nhất quán được áp dụng bên trên các phép suy luận tự động thông thường. Hệ thống OSCAR của John Pollock là một ví dụ về hệ thống lập luận tự động cụ thể hơn so với một hệ thống chứng minh định lý thông thường.
Các công cụ và kỹ thuật của suy luận tự động bao gồm logic cổ điển và các phép tính, logic mờ, suy luận Bayes, suy luận với entropy tối đa và nhiều kỹ thuật ngẫu nhiên không chính thức khác.
Những năm đầu

Sự phát triển của logic hình thức đóng vai trò lớn trong lĩnh vực suy luận tự động, và nó cũng dẫn đến sự phát triển của trí tuệ nhân tạo. Một chứng minh hình thức là một chứng minh mà mọi suy luận logic đều được kiểm tra lại với các tiên đề cơ bản của toán học. Tất cả các bước logic trung gian đều được cung cấp mà không ngoại lệ. Không có sự nhờ cậy vào trực giác, ngay cả khi việc chuyển từ trực giác sang logic là thường xuyên. Do đó, chứng minh hình thức này ít trực giác hơn và ít dễ mắc lỗi logic hơn.
Một số người coi cuộc họp mùa hè Cornell năm 1957, quy tụ nhiều nhà logic học và nhà khoa học máy tính, là khởi đầu của suy luận tự động, hoặc suy luận tự động hóa. Những người khác cho rằng nó bắt đầu trước đó với chương trình Logic Theorist năm 1955 của Newell, Shaw và Simon, hoặc với việc Martin Davis thực hiện quy trình quyết định của Presburger năm 1954 (chứng minh rằng tổng của hai số chẵn là chẵn).
Suy luận tự động, mặc dù là một lĩnh vực nghiên cứu quan trọng và phổ biến, đã trải qua một "mùa đông AI" vào những năm tám mươi và đầu những năm chín mươi. Tuy nhiên, sau đó lĩnh vực này đã hồi sinh. Ví dụ, vào năm 2005, Microsoft đã bắt đầu sử dụng công nghệ xác minh trong nhiều dự án nội bộ của họ và dự định đưa một ngôn ngữ đặc tả logic và kiểm tra (logical specification and checking language) vào phiên bản Visual C năm 2012.
Những đóng góp đáng kể

Principia Mathematica là một tác phẩm mang tính cột mốc trong logic hình thức được viết bởi Alfred North Whitehead và Bertrand Russell. Principia Mathematica - có nghĩa là Nguyên lý của Toán học - được viết với mục đích suy diễn tất cả hoặc một số biểu thức toán học bằng logic ký hiệu. Principia Mathematica ban đầu được xuất bản trong ba tập vào các năm 1910, 1912 và 1913.
Logic Theorist (LT) là chương trình đầu tiên được phát triển vào năm 1956 bởi Allen Newell, Cliff Shaw và Herbert A. Simon nhằm "mô phỏng suy luận của con người" trong việc chứng minh các định lý, và đã được thử nghiệm trên năm mươi hai định lý từ chương hai của Principia Mathematica, chứng minh được ba mươi tám trong số đó. Ngoài việc chứng minh các định lý, chương trình đã tìm ra một chứng minh cho một trong những định lý mà còn thanh thoát hơn so với chứng minh của Whitehead và Russell. Sau một lần không thành công trong việc xuất bản kết quả, Newell, Shaw và Herbert đã báo cáo trong ấn phẩm của họ năm 1958, The Next Advance in Operation Research:
Ví dụ về các chứng minh hình thức
| Năm | Định lý | Hệ thống chứng minh | Người chính thức hóa | Chứng minh truyền thống |
| --- | --- | --- | --- | --- |
| 1986 | Định lý bất toàn thứ nhất | Boyer-Moore | Shankar | Gödel |
| 1990 | Luật tương hỗ bậc hai | Boyer-Moore | Russinoff | Eisenstein |
| 1996 | Định lý cơ bản của giải tích | HOL Light | Harrison | Henstock |
| 2000 | Định lý cơ bản của đại số | Mizar | Milewski | Brynski |
| 2000 | Định lý cơ bản của đại số | Coq | Geuvers et al. | Kneser |
| 2004 | Định lý bốn màu | Coq | Gonthier | Robertson et al. |
| 2004 | Định lý số nguyên tố | Isabelle | Avigad et al. | Selberg-Erdős |
| 2005 | Định lý đường cong Jordan | HOL Light | Hales | Thomassen |
| 2005 | Nguyên lý điểm bất động Brouwer | HOL Light | Harrison | Kuhn |
| 2006 | Flyspeck 1 | Isabelle | Bauer- Nipkow | Hales |
| 2007 | Cauchy Residue | HOL Light | Harrison | Classical |
| 2008 | Định lý số nguyên tố | HOL Light | Harrison | Chứng minh giải tích |
| 2012 | Feit-Thompson | Coq | Gonthier et al. | Bender, Glauberman và Peterfalvi |
| 2016 | Vấn đề bộ ba Pythagoras Boolean | Được chính thức hóa là SAT | Heule et al. | None |
Hệ thống chứng minh

sử dụng Lisp làm logic làm việc.
dựa vào nguyên lý định nghĩa cho các hàm đệ quy toàn phần.
sử dụng rộng rãi việc viết lại và "đánh giá biểu tượng".
một phương pháp suy diễn dựa trên việc thất bại của đánh giá biểu tượng.
Ứng dụng

Suy luận tự động đã được sử dụng phổ biến nhất để xây dựng các hệ thống chứng minh định lý tự động. Tuy nhiên, hệ thống chứng minh định lý thường yêu cầu một số hướng dẫn của con người để hoạt động hiệu quả, vì vậy nó thường được coi là trợ lý chứng minh. Trong một số trường hợp, các hệ thống chứng minh định lý đã đưa ra các cách tiếp cận mới để chứng minh một định lý. Một ví dụ điển hình là chương trình Logic Theorist, chương trình này đã đưa ra một chứng minh cho một trong các định lý trong cuốn *Principia Mathematica* mà ít bước hơn so với chứng minh của Whitehead và Russell. Các chương trình suy luận tự động đang được áp dụng để giải quyết ngày càng nhiều vấn đề trong logic hình thức, toán học và khoa học máy tính, lập trình logic, xác minh phần mềm và phần cứng, thiết kế mạch và nhiều lĩnh vực khác. Thư viện TPTP (Sutcliffe và Suttner 1998) là một thư viện chứa các vấn đề như vậy, được cập nhật thường xuyên. Ngoài ra còn có một cuộc thi giữa các hệ thống chứng minh định lý tự động được tổ chức thường xuyên tại hội nghị CADE (Pelletier, Sutcliffe và Suttner 2002); các vấn đề cho cuộc thi được chọn từ thư viện TPTP.
Prosopocera quadrisignata

| Prosopocera quadrisignata> Phân loại khoa học |
| --- | --- |
Giới (regnum): Animalia
Ngành (phylum): Arthropoda
Lớp (class): Insecta
Bộ (ordo): Coleoptera
Phân bộ (subordo): Polyphaga
Liên họ (superfamilia): Cerambycoidea
Họ (familia): Cerambycidae
Chi (genus): Prosopocera
Loài (species): P. quadrisignata
Danh pháp hai phần
Prosopocera quadrisignata (Chevrolat, 1855) 
Prosopocera quadrisignata là một loài bọ cánh cứng trong họ Cerambycidae.
Chú thích

↑  Bisby, F.A.; Roskov, Y.R.; Orrell, T.M.; Nicolson, D.; Paglinawan, L.E.; Bailly, N.; Kirk, P.M.; Bourgoin, T.; Baillargeon, G.; Ouvrard, D. (2011). “Species 2000 & ITIS Catalogue of Life: 2011 Annual Checklist”. Species 2000: Reading, UK. Truy cập ngày 24 tháng 9 năm 2012.
Trẻ sơ sinh khổng lồ

| --- | --- |
Tiếng Trung: 巨婴 hoặc 巨嬰
Nghĩa chính xác: "Đứa trẻ lớn đầu"
Nguồn gốc: A Country of Giant Infants
Trẻ sơ sinh khổng lồ (tiếng Trung: 巨婴 or 巨嬰), đánh vần là 'ju ying' trong bính âm Hán ngữ, còn được dịch là em bé khổng lồ, là một từ tiếng Trung thông dụng ban đầu có nghĩa là một em bé có kích thước khổng lồ, nhưng hiện nay thường được dùng để mô tả một người lớn chưa trưởng thành về mặt tâm lý. Thuật ngữ này lần đầu tiên được nhà tư vấn tâm lý người Trung Quốc Võ Chí Hồng sử dụng vào năm 2016 trong cuốn sách có tựa đề A Country of Giant Infants (Đất nước của những đứa trẻ sơ sinh khổng lồ).
Trong A Country of Giant Infants, khái niệm này đề cập đến một "đứa trẻ trưởng thành" có thể chất như người lớn nhưng sự phát triển về mặt tinh thần vẫn ở mức độ của một đứa trẻ sơ sinh trước một tuổi. Đất nước do những đứa trẻ khổng lồ này lập nên được gọi là "Quốc gia Em bé khổng lồ".
Những "đứa trẻ sơ sinh khổng lồ" này mắc phải một loạt triệu chứng rối loạn tâm thần – lo lắng, trầm cảm, hoang tưởng, hưng cảm bị ngược đãi, cảm giác bất lực. Chúng được hình thành một cách vô thức. Được chăm sóc không phải là đặc điểm quan trọng nhất của trẻ sơ sinh khổng lồ mà là thiếu cơ hội để trở thành một cá thể độc lập.