本书是有关秦思想史研究专著. 作者通过对儒家早期思想的研究, 从中提炼出"人道"的概念, 作为其理论体系的内核和本书的线索, 并分析了孔子--子思--孟子的思想脉络, 其研究具有一定的气氛性和学术价值.

Ben shu shi guan yu Jiangxi dao jiao yi qian ba bai nian fa zhan shi de tong shi xing zhu zuo,she ji zhong duo de zong pai, ren wu, shi jian, si xiang deng, ju you hen gao de xue shu jia zhi.

本书分电视摄像艺术的技术基础、造型基础、镜语规则与实践三篇。内容有:摄像初步、镜头操作、曝光控制、电视画面造型的基础元素、电视语言等。.

本书以法理学的方法为工具,整合当前我国已有研究成果,比较深入系统地研究了法律控制权的历史地位、重大意义、战略路径和主要机制。.

本书从商品拜物教这一特殊理论视角对现代性的成因、流变、类型及其在当代中国的表现形式做了独特而深入的阐述和分析.

Ben shu yi dao de chuan cheng wei shi jiao,cong yan hui zhi le yu xian, zi gong zhi zhi yu yan, zi lu zhi zhi yu zheng, zi xia zhi xue yu ren si ge fang mian, lun shu zhu xi dui kong zi men ren yan xing de quan shi,cong er jie shi zhu xi dui "Lun yu" zhe yi jing dian suo fan ying de sheng huo shi jie de li jie ji qi he si (...) kao fang shi......shi dui chuan tong zhu xi yan jiu nai zhi song ming li xue yan jiu de yi ge zhong yao bu chong. (shrink)

Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API (...) which can be used to embed it into other systems. It is currently being used to formalize category theory, homotopy type theory, and abstract algebra. We describe the project goals, system architecture, and main features, and we discuss applications and continuing work. (shrink)

Ben shu de zhu yao nei rong shi chan shu zhe xue de te shu de li lun xing zhi he du te de huo dong fang shi,Bing tong guo ju ti lun zheng zhe xue dui gou cheng si xiang de ji ben xin nian,Ji ben luo ji,Ji ben fang shi,Ji ben guan nian,Zhe xue li nian de qian ti pi pan,Zhan xian zhe xue fa zhan de zi wo pi pan de huo li he yong bu ku (...) jie de li lun kong jian. (shrink)

To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover. Lean’s (...) elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and the elaboration algorithm has been carefully designed to balance efficiency and usability. We describe the central design goals, and the means by which they are achieved. (shrink)

Formal verification involves the use of logical and computational methods to establish claims that are expressed in precise mathematical terms. These can include ordinary mathematical theorems, as well as claims that pieces of hardware or software, network protocols, and mechanical and hybrid systems meet their specifications. In practice, there is not a sharp distinction between verifying a piece of mathematics and verifying the correctness of a system: formal verification requires describing hardware and software systems in mathematical terms, at which point (...) establishing claims as to their correctness becomes a form of theorem proving. Conversely, the proof of a mathematical theorem may require a lengthy computation, in which case verifying the truth of the theorem requires verifying that the computation does what it is supposed to do. The gold standard for supporting a mathematical claim is to provide a proof, and twentieth-century developments in logic show most if not all conventional proof methods can be reduced to a small set of axioms and rules in any of a number of foundational systems. With this reduction, there are two ways that a computer can help establish a claim: it can help find a proof in the first place, and it can help verify that a purported proof is correct. Automated theorem proving focuses on the “finding” aspect. Resolution theorem provers, tableau theorem provers, fast satisfiability solvers, and so on provide means of establishing the validity of formulas in propositional and first-order logic. Other systems provide search procedures and decision procedures for specific languages and domains, such as linear or nonlinear expressions over the integers or the real numbers. Architectures like SMT combine domain-general search methods with domain-specific procedures. Computer algebra systems and specialized mathematical software packages provide means of carrying out mathematical computations, establishing mathematical bounds, or finding mathematical objects. A calculation can be viewed as a proof as well, and these systems, too, help establish mathematical claims. Automated reasoning systems strive for power and efficiency, often at the expense of guaranteed soundness. Such systems can have bugs, and it can be difficult to ensure that the results they deliver are correct. In contrast, interactive theorem proving focuses on the “verification” aspect of theorem proving, requiring that every claim is supported by a proof in a suitable axiomatic foundation. This sets a very high standard: every rule of inference and every step of a calculation has to be justified by appealing to prior definitions and theorems, all the way down to basic axioms and rules. In fact, most such systems provide fully elaborated “proof objects” that can be communicated to other systems and checked independently. Constructing such proofs typically requires much more input and interaction from users, but it allows us to obtain deeper and more complex proofs. The Lean Theorem Prover aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains. (shrink)

本书共分六章,包括关于美学学科本性的审思、传统美学的现代转换、跨文化格局中的美学比较、美学作为一种文化批判理论等内容。.

本书内容包括:这个世界怎么了?;自由乎?秩序乎?;都市化乡村?;尴尬的一米线、危难这处谁伸手?;重说雷峰塔的倒掉?;消费者的悲哀?;文凭造假为哪般?等内容。.

本书从时代特征出发,通过大量生动的事实,以及马克思、恩格斯、列宁、毛泽东、邓小平和江泽民同志的著作,论述了马克思主义不断发展的理论。.

本书侧重分析中华民族哲学智慧的个性及其对人类哲学文明发展的特殊贡献。中华文明从未间断并发展下来的哲学原因是中华民族不断开发不断完善的直观智慧,中华民族的哲学精神为人类简单明了地指出了走出民族冲突与宗教 冲突困惑的思路。.

This article proposes a comparative and typological study of predicative demonstratives in French, Mandarin Chinese and Vietnamese. Six class of predicative demonstratives have been described one after another: presentive demonstratives, identification demonstratives, localizing demonstratives, copular demonstratives, manner demonstratives and implicit demonstratives. This research makes it possible to underline the syntactic and semantic characteristics of predicative demonstratives in the three languages, in the sense that they often function as non-verbal predicates without subjects and playing a role of reference or discourse-pragmatics. The (...) predicative demonstratives in Mandarin Chinese and Vietnamese have another particularity because a demonstrative morpheme can be used in several morphosyntactic categories. (shrink)

Este texto parte de una escena, de una situación compleja y singular que expone Bergson al principio de su Ensayo sobre los datos inmediatos de la conciencia. Se trata del párrafo en el que habla sobre el sentimiento estético de la gracia, en relación con la contemplación de un cuerpo danzante. A partir de una lectura atenta de este pasaje podemos repensar el concepto de duración bergsoniano, comprendiendo su dimensión relacional y continua; en otras palabras, su dimensión rítmica. La danza (...) funcionará como una posible imagen mediadora entre estos conceptos. (shrink)

作为一个全新的时代课题,孔子与传播学扯在一起颇有些奇意。《论语》所记载的,是孔子从生活中演绎出来的为人处世的经验和他对弟子的教导。这部曾经被古人誉为治国之本的儒家经典为现代人构建和谐社会,建立良好的人 际关系,提供一份温馨的劝导。开办学校、讲学、授业解惑、删诗修史、整理文献典籍、周游列国传播自己的理想和学说,可以说孔子整个一生都在传播。生命即传播,传播即生命,这就是孔子的人生.

1. Juan shou -- 2. Da zong hu zhi yi -- 3. Da zong hu zhi er -- 3. Linyi hu. Mengcun hu -- 4. Daogou hu -- 6. Tengyang hu zhi yi -- 7. Tengyang hu zhi er -- 8. Jiu Xian hu -- 9. Zhongji hu -- 10. Caizhuang hu. Daizhuang hu. Liyuan hu -- 11. Shizhuang hu. Sibei hu -- 12. Dianbei hu. Xiguo hu -- 13. Xianyuan hu. Quannan hu. Qiwang hu. Chengguo hu -- 14. Miaokong (...) hu. Wenxian hu. Yibei hu -- 15. Hongmen hu. Shi Cun hu. Luxian hu. Yiyang hu. Kong Cun hu. Wangtang hu. Xiaozhuang hu. Gongduan hu -- 16. Huadian hu -- 17. Gucheng hu. Gangshan hu -- 18. Lucheng hu zhi yi -- 19. Lucheng hu zhi er -- 20. Kongtun hu. Xicheng hu. Jiucheng hu -- 21. Lüguan hu zhi yi -- 22. Lüguan hu zhi er -- 23. Lüguan hu zhi san -- 24. Lüguan hu zhi si -- 25. Linqian hu. Fangxi hu. Linmen hu -- 26. Guanzhuang hu. Daxue hu -- 27. Guangwen hu -- 28. Xiaoxue hu. Taole hu. Beigong hu -- 29. Zhifang hu. Dongzhuang hu. Fangshang hu. Gaozhuang hu. Nangong hu -- 30. Xing Cun hu. Guliu hu. Wu Sun hu. Dong Cun hu. Mozhuang hu -- 31. Zhangqu hu. Xizou hu -- 32. Xilin hu. Linxi hu -- 33. Nanzong pai -- 34. Jiangxi Xinjian zhi. Sichuan Langzhong zhi. Zhejiang Wenling zhi. Zhejiang Qiantang zhi -- 35. Qingping Kongzhuang zhi. Guangdong Nanhai Dali zhi. Henan Taikang zhi --. (shrink)

Commented article: LIU, Z. The Concept of Music Education from a Philosophical Perspective. Trans/Form/Ação: revista de filosofia da Unesp, v. 47, n. 5, “Eastern thought 2”, e02400161, 2024. Available at: https://revistas.marilia.unesp.br/index.php/transformacao/article/view/15083.

本书介绍了“三个代表”重要思想是新世纪“指导自己前进的真理”;“三个代表”重要思想是对马克思主义的新发展;“三个代表”重要思想的科学内涵和内在关联;继续为实现党的基本路线和历史任务面奋斗等。.