Can all the logic systems be manually re-created in the form of some artificial intellegence tools such as computers?
Are all the human knowlege representable in some form of logics?
Can the human capability of finding new knowledge be representable in some form of logics?
Reference 1
A pursuit for the principles of logics, before computers exist.
Imagine it’s your first internship, and you are asked to write a max() method for an IntList class. You write this code and bring it to your boss. She says, “Prove to me that it works.” OK… how do you do that? You could (and surely would) run some tests on sample input, but there’s effectively an infinite number of possible IntLists. Tests are useful, but they can’t prove that your code works in all possible scenarios.
This is where reasoning about code comes in.
Instead of running your code, you step back and read it. You ask:“What is guaranteed to be true at this point in the program, based on the statements before it?” Or, going in the other direction:“If I want to guarantee that some fact Q is ture at this point in the program, what must be true earlier to provide that guarantee?” You have surely done some of this naturally. Now you’ll learn to do it in a more structured way with techniques to help.
References: Software Foundations [Video Class, Benjamin C. Pierce]() Video Class2, Micheal Ryan Clarkson @ Cornell Peking, Software foundations Building reliable software is really hard – really hard. The scale and complexity of modern systems, the number of people involved, and the range of demands placed on them make it challenging to build software that is even more-or-less correct, much less 100% correct. At the same time, the increasing degree to which information processing is woven into every aspect of society greatly amplifies the cost of bugs and insecurities.
References: Concrete Semantics Imperative language Statement: declaration of fact or claim. e.g. “Semantics is easy.” 声明/断言：对一个事实或者断言的声明。比如，“语义学是简单的”。 Command：order to do something. e.g. “Study the book until you have
Top Wonderings Formal logic vs informal logic, how can they assist the artificial intelligence/life in general? The representation of the knowledge(model, data, algorithms, problems, etc)? What kind of representations under the hood? Reference 1： 逻辑学从哲学中独立出来的趋势以后便被人们发现是属于数学。因此当把作为数
Reference: An Overview of Formal Methods Tools and Techniques. Rigorous Software Development: An Introduction to Program Verification. 2011. Survey of Approches for Security Verification of Hardware/Software Systems. Onur Demir, Wenjie Xiong, Faisal Zaghloul, Jakub Szefer. 2016. pdf Wiki: Formal Verification Formal Methods 一文读懂基于SCADE模型的形式化方法 形式化方法是一种用
Q&A How formal methods are used in the architectural design (IC/ASIC/FPGA)? References: Part8: The 2018 Wilson Research Group Functional Verification Study IC/ASIC adoption trends for formal property checking (e.g., model checking), as well as automatic formal applications: formal property checking: Model checking; automatic formal application tools: SoC integration connectivity checking; deadlock detection; X semantic safety checks; coverage reachability analysis; many other properties that can be automatically extracted and then formally proven.
References: More More Kami References Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Kami: A Framework for (RISC-V)HW Verification Coq Reference: The Coq Proof Assistant Isabelle advantages over Coq: From Benjamin Pierce notion of equality is extensional; it eliminates a lot of low-level tedium in proofs of involves equality. a much better story about variable binding; formalizing sth that involves binding variables.
Intro Logic 2nd Ph.D. student. (Germany) 6 and 3 and another one on the way. Text book: Statement Logic Predicate Logic Logic is the study of methods for evaluating whether the premises of an argument adequately support its conclusion. An argument is a set of propositions where some of the propositions are intended to support another one in the set. A proposition a truth or falsehood that may or may not be expressed in a sentence.
References: Match 220, Formal Methods, Stan Warford @ Pepperdine University. State: a list of variables and there values. Textual substitution (x + 2y) [x,y := y,x] is not the same as (x + 2y) [x := y] [y := x] ==> the property of textual substitution. Example: ((a + b) x ) [b:=x] [x:=b] ==> (a + b) b ((a + b) c) [b:=x] [x:=b] ==> (a + b) c —> Provisal (provided that…)
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?