目录
28 关系: ACM，ACM软件系统奖，AMD K5，子程序，定理机器证明，一阶逻辑，开源软件，归纳推理，全集，元编程，副作用，BSD许可证，Common Lisp，硬件，編譯器，罗克韦尔柯林斯，猜想，甲骨文公司，類型系統，證明，超威半导体，软件，重写逻辑，自动推理，自洽，英特尔，IBM，Pentium FDIV bug。
- LISP程式語言
- LISP程式語言家族
ACM
ACM可以指：.
查看 ACL2和ACM
ACM软件系统奖
ACM软件系统奖（ACM Software System Award）是美国计算机协会（ACM）颁发的一项奖项，它授予对技术概念和商业接受度方面产生了持久影响的软件系统的开发者或机构。该奖始于1983年，每年颁发一次，目前奖金已达3.5万美元，由IBM公司提供赞助。.
AMD K5
K5是一個由AMD製作與Intel推出的Pentium競爭的產品，由Mike Johnson主導整個K5處理器開發計畫。整个K5项目看起来更像是AMD面对INTEL突然推出跨时代的Pentium处理器措手不及的应对之作。其性能较Pentium处理器有较大差距。.
查看 ACL2和AMD K5
子程序
在计算机科学中，子程式（Unterprogramm, Subroutine, procedure, function, routine, method, subprogram, callable unit），是一個大型程式中的某部份程式碼，由一个或多个语句块组成。它負責完成某項特定--，而且相較於其他程式碼，具備相對的獨立性。 一般会有输入参数并有--，提供对过程的封装和细节的隐藏。这些代码通常被整合为软件库。 函数在-zh:程序導向;zh-tw:程序導向;zh-cn:面向过程-的语言中已经出现。是结构（Struct）和-zh:類別;zh-tw:類別;zh-cn:类-（Class）的前身。本身就是对具有相关性语句的归类和对某过程的抽象。.
查看 ACL2和子程序
定理机器证明
定理机器证明（Automated theorem proving，簡稱ATP）目前是自动推理（Automated reasoning，簡稱AR）体系中发展最好的部分，它的目的是为使用电子计算机程序来进行数学定理的证明。对于不同的数学逻辑，它能够推论出一个定理是正确的，还是不可证明的，或者错误的。 Category:数学软件.
查看 ACL2和定理机器证明
一阶逻辑
一阶逻辑是使用於数学、哲学、语言学及電腦科學中的一种形式系统。 過去一百多年，一階邏輯出現過許多種名稱，包括：一阶斷言演算、低階斷言演算、量化理論或斷言逻辑（一個較不精確的用詞）。一階邏輯和命題邏輯的不同之處在於，一階邏輯有使用量化變數。一個一階邏輯，若具有由一系列量化變數、一個以上有意義的斷言字母及包含了有意義的斷言字母的純公理所組成的特定論域，即是一個一階理論。 一階邏輯和其他高階邏輯不同之處在於，高階邏輯的斷言可以有斷言或函數當做引數，且允許斷言量詞或函數量詞的（同時或不同時）存在。在一階邏輯中，斷言通常和集合相關連。在有意義的高階邏輯中，斷言則會被解釋為集合的集合。 存在許多對一階邏輯是可靠（所有可證的敘述皆為真）且完備（所有為真的敘述皆可證）的演繹系統。雖然一階邏輯的邏輯歸結只是半可判定性的，但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的元邏輯定理，如勒文海姆–斯科倫定理及緊緻性定理。 一階邏輯是數學基礎中很重要的一部份，因為它是公理系統的標準形式邏輯。許多常見的公理系統，如一階皮亞諾公理和包含策梅洛-弗蘭克爾集合論的公理化集合論等，都可以形式化成一階理論。然而，一階定理並沒有能力去完整描述及範疇性地建構如自然數或實數之類無限的概念。這些結構的公理系統可以由如二階邏輯之類更強的邏輯來取得。.
查看 ACL2和一阶逻辑
开源软件
开源软件（open source software，英文缩写：OSS，中文也称：开放源代码软件）是一种源代码可以任意--的计算机软件，这种软件的版权持有人在软件协议的规定之下保留一部分权利并允许用户学习、修改、增进提高这款软件的质量。开源协议通常符合開放原始碼的定義的要求。一些开源软件被发布到公有领域。开源软件常被公开和合作地开发。开源软件是开放源代码开发的最常见的例子，也经常与用户-zh-hans:生成; zh-tw:創作-内容做比较。 开源软件的英文“open-source software”一词出自自由软件的营销活动中。 开源软件同时也是一種軟體散佈模式。一般的軟體僅可取得已經過編譯的二進位可執行檔，通常只有軟體的作者或著作權所有者等擁有程式的原始碼。 有些軟體的作者只將原始碼公開，卻不符合「開放原始碼」的定義及條件，因為作者可能設定公開原始碼的條件限制，諸如限制可閱讀原始碼的對象、限制衍生產品等，此稱之為公开源代码的免费软件（Freeware，例如知名的模擬器軟體MAME），因此公開原始碼的軟體並不一定可稱之為開放原始碼軟體。.
查看 ACL2和开源软件
归纳推理
归纳法或归纳推理（Inductive reasoning），有时叫做归纳逻辑，是论证的前提支持结论但不确保结论的推理过程。它基于对特殊的代表（token）的有限观察，把性质或关系归结到类型；或基于对反复再现的现象的模式（pattern）的有限观察，公式表达规律。例如，使用归纳法在如下特殊的命题中：.
查看 ACL2和归纳推理
全集
数学上，特别是在集合论和数学基础的应用中，全类（若是集合，则为全集）大约是这样一个类，它（在某种程度上）包含了所有的研究对象和集合。.
查看 ACL2和全集
元编程
元編程（英語：Metaprogramming），又譯超編程，是指某类计算机程序的编写，这类计算机程序编写或者操纵其它程序（或者自身）作为它们的資料，或者在运行时完成部分本应在编译时完成的工作。多数情况下，与手工编写全部代码相比，程序员可以获得更高的工作效率，或者给与程序更大的灵活度去处理新的情形而无需重新编译。 编写元程序的语言称之为元语言。被操纵的程序的语言称之为「目标语言」。一门编程语言同时也是自身的元语言的能力称之为「反射」或者「自反」。 反射是促进元编程的一种很有价值的语言特性。把编程语言自身作为一級資料類型（如LISP、Forth或Rebol）也很有用。支持泛型编程的语言也使用元编程能力。 元编程通常通过两种方式实现。一种是通过应用程序编程接口（APIs）将运行时引擎的内部信息暴露于编程代码。另一种是动态执行包含编程命令的字符串表达式。因此，“程序能够编写程序”。虽然两种方式都能用于同一种语言，但大多数语言趋向于偏向其中一种。.
查看 ACL2和元编程
副作用
在醫學中，副作用（英語：side effect）是指藥品往往有多種作用，作用於不同身體部位受體，治療時利用其一種或一部分受體作用，其他作用或是受體產生作用即變成為副作用。雖然副作用一詞常被用來形容 不良反应 (医学)，但事實上副作用也可以指那些「有益處、意料之外」的效果。 有時候，一些藥物的副作用反而成為醫生處方那些藥物的目的；在這種情況下，那些藥物的副作用不再是副作用，反而是藥物的主作用了。 例如：X輻射線/X光一直被用做醫學影像用途，人們原本把它的輻射線對人體產生的效果當成是副作用。但自從人們發現X輻射線/X光能夠用來治療腫瘤後，輻射線被應用為放射線療法。在醫學影像領域中被當成副作用的輻射線效果，在癌症治療上反而成了消滅贅生物的正作用了。.
查看 ACL2和副作用
BSD许可证
BSD 授權條款（Berkeley Software Distribution license），是自由軟體中使用最廣泛的授權條款之一。BSD 就是遵照這個許可證來發布，也因此而得名 BSD 授權條款。 BSD 套件最初所有者是加州大學的董事會，這是由於 BSD 源自加州大學伯克利分校。BSD 開始後，BSD 授權條款得以修正，使得以後許多 BSD 變種，都采用類似風格的條款。 跟其他條款相比，從GNU通用公共許可證（GPL）到限制重重的著作權（Copyright），BSD許可證比較寬松，甚至跟公有領域更為接近。事實上，BSD許可證被認為是copycenter（中間版權），介乎標準的copyright與GPL的copyleft之間。"Take it down to the copy center and make as many copies as you want"。可以說，GPL強迫後續版本必須一樣是自由軟體，BSD的後續版本可以選擇要繼續是BSD或其他自由軟體條款或封閉軟體等等。.
查看 ACL2和BSD许可证
Common Lisp
Common Lisp，縮寫為CL（不是組合邏輯的縮寫）是Lisp編程語言的一種方言，由ANSI INCITS 226-1994(R2004)（前身為ANSI X3.226-1994(R1999)），所定義的語言規範標準。Common Lisp HyperSpec是源自於ANSI Common Lisp標準的網頁超連結版本。 CL語言是為標準化和改良Maclisp而開發的後繼者。到20世紀80年代初，幾個工作群組已經在設計MacLisp各種後繼者，例如：Lisp Machine Lisp（又名 ZetaLisp），Spice Lisp，NIL和S-1 Lisp。CL是為了標準化和擴展此前眾多的MacLisp分支而開發，它本身並非具體的實作，而是對語言設立標準的規範。有數個實作符合Common Lisp規範，其中包括自由和開源軟件，以及商業化產品。CL支援了結構化、函數式和物件導向編程等範式。相对于各种嵌入在特定产品中的语言，如Emacs Lisp和AutoLISP，Common Lisp是一種用途廣泛的编程语言。不同於很多早期Lisp，Common Lisp如同Scheme，其中的變量是預設為詞法作用域的。 身為一種動態編程語言，它有助於進化和增量的軟件開發，並將其迭代編譯成高效的執行程序。這種增量開發通常是互動持續地改善，而不需中斷執行中的應用程序。它還支援在後期的分析和優化階段添加可選的型別註記與轉型，使編譯器產生更有效率的代碼。例如在硬體和實作的支援範圍內，fixnum能保存一個未封裝整數，允許比大整數或任意精度類型更高效率的運算。同樣地，在每個模組或函數的基礎上可聲明優化，指示編譯器要編譯成哪一類型的安全級別。 CL包含了支援多分派和方法組合的物件系統，縮寫為CLOS，它通常以元物件（Metaobject）協定來實現。 CL藉由標準功能進行擴展，例如Lisp宏（编译时期程序自身完成的代码重排（compile-time code rearrangement accomplished by the program itself））和阅读器宏（赋予用户自定义的語法以扩展具特殊意义的符号（extension of syntax to give special meaning to characters reserved for users for this purpose））。 CL為Maclisp和约翰·麦卡锡的原創Lisp提供了一些向後兼容性。這允許較舊的Lisp軟件移植到Common Lisp之上。.
硬件
是裝置在機箱內以做出個人電腦。系統軟體是儲存在硬體內，而系統軟體內含有韌體，例如BIOS以及作業系統，這些軟體使應用軟體可以提供使用者所需的功能。作業系統通常藉由匯流排與裝置溝通，這需要軟體提供驅動程式。.
查看 ACL2和硬件
編譯器
编译器（compiler），是一種電腦程式，它會將用某種程式語言寫成的原始碼（原始語言），轉換成另一種程式語言（目標語言）。 它主要的目的是將便于人编写、阅读、维护的高级计算机语言所寫作的原始碼程式，翻译为计算机能解读、运行的低阶机器语言的程序，也就是執行檔。编译器将原始程序（source program）作为输入，翻译产生使用目标语言（target language）的等价程序。源代码一般为高阶语言（High-level language），如Pascal、C、C++、C# 、Java等，而目标语言则是汇编语言或目标机器的目标代码（Object code），有时也称作机器代码（Machine code）。 一个现代编译器的主要工作流程如下： 源代码（source code）→ 预处理器（preprocessor）→ 编译器（compiler）→ 汇编程序（assembler）→ 目标代码（object code）→ 链接器（Linker）→ 執行檔（executables）， 最後打包好的檔案就可以給電腦去判讀執行了。.
查看 ACL2和編譯器
罗克韦尔柯林斯
罗克韦尔柯林斯（Rockwell Collins, Inc.）是美国一家大型的国际化公司，主要提供航空电子、信息系统等。 2017年9月5日聯合技術公司以每股93.33美元現金和價值46.67美元的联合技術股票，合共每股140美元，斥資230億美元收購同業羅克韋爾柯林斯（Rockwell Collins）。若計入淨債務，交易價值高達300億美元。交易完成后，羅克韋爾柯林斯與聯合技術公司的航空系统部門将合併成為一家名為“柯林斯航空系统”的新公司。.
查看 ACL2和罗克韦尔柯林斯
猜想
數學中的猜想是在根據不完全資訊下的結論及命题，是不知其真假的數學敘述，它可能為真，暫時未被證明或反證 。某些猜想會稱為「假設」，尤其是當它是針對某些問題提出的答案。 像黎曼猜想（目前仍然是猜想）或是費馬最後定理（以往是猜想，一直到1995年才得證）都對數學歷史帶來許多的進展，而且為了證明這些猜想，也發展了新的數學領域。 當猜想被證明後，它便會成為定理。猜想只要未成為定理，數學家都要小心在邏輯結構之中使用這些猜想。猜想主要因為類比推理和偶然發現的巧合而出現。數學家通常會使用不完全歸納法，來測試自己的猜想。例如費馬曾經根據首四個費馬數是素數，便猜想所有費馬數都是素數（此猜想已被推翻）。.
查看 ACL2和猜想
甲骨文公司
文股份有限公司（Oracle，）是一間全球性的大型企業軟件公司。总部位于美国加州红木城的紅木岸（Redwood Shores），現時行政總裁為公司創辦人劳伦斯·埃里森（Lawrence J. Ellison）。直到2013年为止，甲骨文是繼微软後，全球收入第二多的软件公司。.
查看 ACL2和甲骨文公司
類型系統
在计算机科学中，--系統用于定義如何將程式語言中的數值和zh:運算式;zh-tw:運算式;zh-cn:表达式-归類为许多不同的型別，如何操作这些型別，这些型別如何互相作用。型別可以确认一个值或者一组值具有特定的意义和目的（雖然某些型別，如抽象型別和--型別，在----中，可能不表示為值）。型別系統在各種語言之間有非常大的不同，也許，最主要的差異存在於編譯時期的語法，以及執行時期的操作实现方式。 編譯器可能使用值的靜態型別以最佳化所需的儲存區，並選取對值運算時的較佳演算法。例如，在許多C編譯器中，「浮點數」資料型別是以32 位元表示，與IEEE 754規格一致的單精度浮點數。因此，在數值運算上，C應用了浮點數規範（浮點數加法、乘法等等）。 型別的約束程度以及評估方法，影響了語言的型別。更進一步，程式語言可能就型別多態性部分，對每一個型別都對應了一個極度個別的演算法的運算。型別理論研究型別系統，儘管實際的程式語言型別系統，起源於電腦架構的實際問題、編譯器實作，以及語言設計。.
查看 ACL2和類型系統
證明
在數學上，證明是在一個特定的公理系統中，根据一定的规则或标准，由公理和定理推導出某些命題的過程。比起证据，数学证明一般依靠演绎推理，而不是依靠自然归纳和经验性的理据。這樣推導出來的命題也叫做該系統中的定理。 數學證明建立在逻辑之上，但通常會包含若干程度的自然語言，因此可能會產生一些含糊的部分。實際上，用文字形式寫成的數學證明，在大多數情況都可以視為非形式邏輯的應用。在證明論的範疇內，則考慮那些用純形式化的语言写出的證明。這個区别导致了对過往到現在的數學实践、和的大部分检验。數學哲學就關注語言和邏輯在數學證明中的角色，和作為語言的數學。.
查看 ACL2和證明
超威半导体
超微半导体公司（Advanced Micro Devices, Inc.；縮寫：AMD、超微，或譯「超威」），創立於1969年，是一家專注於微处理器及相關技術設計的跨国公司，总部位于美國加州舊金山灣區矽谷內的森尼韦尔市。最初，超微擁有晶圓廠來製造其設計的晶片，自2009年超微將自家晶圓廠拆分為現今的GlobalFoundries（格羅方德）以後，成為無廠半導體公司，僅負責硬體積體電路設計及產品銷售業務。現時，超微的主要產品是中央處理器（包括嵌入式平台）、圖形處理器、主機板晶片組以及電腦記憶體， 超微半導體是目前除了英特爾以外，最大的x86架構微處理器供應商，自收購冶天科技以後，則成為除了輝達以外僅有的獨立圖形處理器供應商，自此成为一家同時擁有中央處理器和圖形處理器技術的半導體公司，也是唯一可与英特爾和輝達匹敵的廠商。在2017年第一季全球個人電腦中央處理器的市場佔有率中，英特爾以79.8％排名第一、AMD以20.2％位居第二。於2017年8月，AMD CPU在德國電商Mindfactory的銷售量首次以54.0%超越intel，並於9月增長至55.0%，於10月(同時也是Coffee Lake推出之月份)，銷售份額仍繼續成長至57.7%，於11月，由於增加部分未計算型號，份額下降至57.4%.
查看 ACL2和超威半导体
软件
軟體（software）是一系列按照特定顺序组织的電腦数据和指示，是電腦中的非有形部分。電腦中的有形部分稱為硬體，由電腦的外殼及各零件及電路所組成。電腦軟體需有硬體才能運作，反之亦然，軟體和硬體都無法在不互相配合的情形下進行實際的運作。 一般来說，计算机软件划分为程式語言、系统软件、应用软件和介于这两者之间的中介軟體。其中系统软件为计算机使用提供最基本的功能，但是并不针对某一特定应用领域。而应用软件则恰好相反，不同的应用软件根据用户和所服务的领域提供不同的功能。 软件包括所有在電腦執行的程式，和其架構無關，例如執行檔、函式庫及腳本語言都屬於软件。軟體不分架構，有其共通的特性，在執行後可以讓硬體執行依設計時要求的機能。軟體儲存在記憶體中，軟體不是可以碰觸到的實體，可以碰觸到的都只是儲存軟體的零件（記憶體）或是媒介（光碟或磁片等）。 软件并不一定只包括可以在计算机上运行的電腦程式，有些定義中，与電腦程式相关的文档，一般也被认为是软件的一部分。简单的说软件就是程式加文档的集合体。软件被应用于世界的各个领域，对人们的生活和工作都产生了深远的影响。.
查看 ACL2和软件
重写逻辑
重写逻辑是一种对绝大多数编程语言和系统进行规范描述的计算机逻辑。重写逻辑能把目标逻辑的抽象语法表示为代数结构。利用重写规则，目标逻辑的推理规则可以被描述出来。 重写逻辑中的语法和结构化公理都由用户自己定义，这使其变得极为简单且通用。 1992年，José Meseguer在《作为统一并发模型的条件重写逻辑》一文中首先提出重写逻辑这一概念。.
查看 ACL2和重写逻辑
自动推理
自动推理是计算机科学和数理逻辑的一个交叉领域，致力于了解理智的方方面面。自动逻辑的研究帮助了利用计算机自动进行完全或几乎完全的推理，其內容一般可分為演繹推理和非演繹推理。自动推理被认为是人工智能的一个分支，还和理论计算机科学甚至哲学相关联。 自动推理的研究内容包括定理机器证明、证明自动检查、不确定性推理、非单调推理以及类比归纳和外展推理。 自动推理的技术和工具包括经典逻辑、微积分学、模糊逻辑、贝叶斯推断、推理与最大熵和大量的非正式特别技术。 Category:理论计算机科学 Category:人工智能 Category:计算机逻辑 Category:推理.
查看 ACL2和自动推理
自洽
#重定向 一致性 (邏輯).
查看 ACL2和自洽
英特尔
英特爾公司（Intel Corporation，、）是世界上最大的半導體公司，也是第一家推出x86架構處理器的公司，總部位於美國加利福尼亞州聖克拉拉。由羅伯特·諾伊斯、高登·摩爾、安迪·葛洛夫，以“集成電子”（Integrated Electronics）之名在1968年7月18日共同創辦公司，將高階晶片設計能力與領導業界的製造能力結合在一起。英特爾也有開發主機板晶片組、網路卡、快閃記憶體、繪圖晶片、嵌入式處理器，與對通訊與運算相關的產品等。“Intel Inside”的廣告標語與Pentium系列處理器在1990年代間非常成功的打響英特爾的品牌名號。 英特爾早期在開發SRAM與DRAM的記憶體晶片，在1990年代之前這些記憶體晶片是英特爾的主要業務。在1990年代時，英特爾做了相當大的投資在新的微處理器設計上與培養快速崛起的PC工業。在這段期間英特爾成為PC微處理器的供應領導者，而且市場定位具有相當大的攻勢與有時令人爭議的行銷策略，就像是微軟公司一樣支配著PC工業的發展方向。而Millward Brown Optimor發表的2007年在世界上最強大的品牌排名顯示出英特爾的品牌價值由第15名掉落了10個名次到第25名。 而主要競爭對手有AMD、NVIDIA及Samsung。.
查看 ACL2和英特尔
IBM
国际商业机器股份有限公司（International Business Machines Corporation，首字母縮略字：IBM，曾译万国商用机器公司）是美國一家跨國科技公司及諮詢公司，總部位於紐約州阿蒙克市。IBM主要客户是政府和企业。IBM生产并销售计算机硬件及软件，并且为系统架构和网络托管提供咨询服务。截止2013年，IBM已在全球拥有12个研究实验室和大量的软件开发基地。IBM雖然是一家商業公司，但在材料、化学、物理等科学领域卻也有很高的成就，利用這些學術研究為基礎，发明很多产品。比较有名的IBM发明的产品包括硬盘、自動櫃員機、通用产品代码、SQL、关系数据库管理系统、DRAM及沃森。.
查看 ACL2和IBM
Pentium FDIV bug
#重定向 奔腾浮点除错误.