Quote: the principles of logic and mathematics are true because they arise from the rules that govern the use of language; they are analytical [»ayerAJ_1956]

Quote: mathematics and logic are part of the apparatus of language, not part of its application; allows us to use "900" in our daily life [»wittL_1939]

Quote: a theory of meaning should define meaning by a finite number of applications of a finite number of rules on a finite vocabulary [»daviD_1968]

Quote: human reason regards all knowledge as parts of a possible system and hence resists contradiction; but there is no system [»kantI_1781, OK]

Quote: the faculty of reason has a natural desire to build a self-subsistent systematic whole by ideas alone [»kantI_1781, OK]

Quote: Speciosa Generalis reduces truth and reason to a calculus of characters and words; a universal language, easily learned [»leibGW3_1714]

Quote: a Speciosa Generalis would guide reasoning, avoid errors, and estimate probabilities

Quote: through mathematical analysis, there is no problem that cannot be solved [»vietF_1591]

Quote: Leibniz's goal: to conceive all propositions in the form of terms [»leibGW_1686]

Quote: Hobbes--everything done by our mind is a computation; 'is' and 'is not' corresponds to + and - [»leibGW_1666]

Quote: all of reasoning may be conducted by symbols, operations, and identity; closely related to algebra [»boolG_1854, OK]

Quote: there is no inherent limitation to the intelligence of a computer program; e.g., Post's automatic improvement process for deciding if a sentence is a theorem [»mccaJ8_1962]

Quote: to reason correctly with symbols, translate using a fixed interpretation, formally manipulate the symbols, and translate back the result [»boolG_1854, OK]

Quote: reducing an argument to symbolic form determines its real premises, detects ambiguities [»boolG_1854, OK]

Quote: with symbolic logic, the process of inference is precise, almost mechanical

Quote: by pure thought can derive propositions about sequences that far surpass in generality those derived by intuition or the senses [»fregG_1879]

Quote: a small number of laws and rules can include the content of all the laws, albeit in an undeveloped state [»fregG_1879]

Quote: derive complex judgments from simpler ones; clarifies relationships

Quote: all of psychology is based on the activity of neuron nets, i.e., on two-valued logic [»mccuWS_1943]

Quote: mathematical logic is seldom used in proofs; it should be a calculational alternative to human reasoning [»dijkEW12_1989]

Quote: formal reasoning concerns statements that do not mention actual things; e.g., if all alphas are betas and x is an alpha than x is a beta [»russB_1919, OK]

Quote: absolute and hypothetical truths have the same laws; syllogisms are categorical

Quote: for every true universal, affirmative, categorical proposition the predicate is contained numerically in the subject [»leibGW4_1679]

Quote: the true is what can be proved or analyzed; the false is what is contrary [»leibGW_1686]

Quote: the necessary reduces to an identity; the impossible reduces to a contradiction; the possible is not impossible

Quote: a false term leads to contradiction; a true term does not

Quote: necessary truths are those that reduce to identity; impossibles are those that lead to contradiction [»leibGW_1686]

Quote: to be certain of truth, analyze to the fundamentally true or prove that a contradiction will never occur; the latter can eliminate a long continuation [»leibGW_1686]

Quote: from truth, falsity never follows, but from an impossibility, anything follows -- not used [»ockhW_1310]

Quote: can reduce any system of logical equations to a single, equivalent equation [»boolG_1854, OK]

Quote: a proposition is true a priori when it is reducible to identical propositions; its reason always appears [»leibGW_1679]

Quote: infinite things can be compounded out of the combination of a few; e.g., numbers from digits [»leibGW_1679]

Quote: mathematical analysis uses the art and rules of logic to obtain equations of species (e.g., 'x') instead of numbers [»vietF_1591]

Quote: use GAWK for AI because any logic merely defines how strings can be transformed into other strings; GAWK is designed for string transformation [»louiRP8_1996]

Quote: the stack principle grew out of checking well-formed, propositional formula using Plankalkul [»baueFL_2002]

Quote: an inference principle needs to be sound (i.e., allow only logical consequences) and effective (i.e., algorithmically decidable)

Quote: all uses of the variable 'x' can be transformed into qualification, classes, functions, or combinators; e.g., singular description [»quinWV2_1947]

Quote: universal qualification by indicating that a function is a fact for any replacement of a sign [»fregG_1879]

Quote: form existential qualification out of negation and universal qualification [»fregG_1879]

Quote: in a denoting phrase, 'the' becomes an uniqueness qualification; makes for involved rewordings [»russB_1956]

Quote: universal qualification needs to specify its scope [»fregG_1879]

Quote: a logic clause is the same as 'for all x1..xk B1 or ... or x1..xk Bm is implied by A1 and ... and An' [»kowaR11_1973]

Quote: in paper solutions, negation seldom used; e.g., 'and' appeared 6.1 times per participant while 'not' appeared 0.1 times [»paneJF2_2001]

Quote: those propositions are necessary whose contrary implies a contradiction [»leibGW_1679]

Quote: implication in first-order logic can be replaced by unsatisfiability of sentences in clausal form [»kowaR11_1973]

Quote: survey of propositional satisfiability (SAT) and constraint programming (CP); similarities and differences [»bordL12_2006]

Quote: a formal framework for discovering inconsistency errors with a boolean SAT solver; e.g., 600 null dereferences in Linux [»dillI6_2007]

Quote: order the inductive numbers by: m<n if n possesses every hereditary property possessed by the successor of m [»russB_1919, OK]

Quote: resolution may be the first complete system of first-order logic using just one inference principle [»robiJA1_1965]

Quote: the resolution principle -- from any two clauses, one may infer a resolvent; a refutation is a sequence of resolutions leading to the empty clause; unsatisfiable iff refutation [»robiJA1_1965]

Quote: analyze and simplify relay networks as equations; equivalent to calculus of propositions; produces minimal, series and parallel networks

Quote: X' is the negative of X, i.e., the break contacts of a relay; X+X'=1 [»shanCE6_1938]

Quote: perfect analogy between calculus of switching circuits and Boolean logic; Huntington's postulates and De Morgan's theorem [»shanCE6_1938]

Quote: simplify series-parallel circuits by using Shannon's theorems to reduce the number of letters in the expression

Quote: use truth tables to prove theorems about hindrances, i.e., open or closed circuits; e.g., associative and distributive laws [»shanCE6_1938]

Quote: replace the concepts of subject and predicate with argument and function respectively [»fregG_1879]

Quote: Frege does not use subject/predicate because it is part of the interaction between speaker and listener [»fregG_1879]

Quote: Begriffschrift introduced truth-functional propositional calculus, functions instead of subject/predicate, quantification, derivational forms, and a definition of sequence [»fregG_1879]

Quote: Frege only uses detachment to infer consequences; other modes of inference are equivalent [»fregG_1879]

Quote: two of Frege's basic laws are excluded middle and reduction of implication; substitution rules are unstated [»fregG_1879]

Quote: Frege's rule V allows substitution of equivalents [»fregG_1879]

Quote: Boole uses and, or, not, and complement; communtative law and idempotent law [»boolG_1854, OK]

Quote: only 0 and 1 satisfy x^2=x; algebra of 0 and 1 is the same as the algebra of logic with a new interpretation [»boolG_1854, OK]

Quote: get the law of contradiction from x^2=x [»boolG_1854, OK]

Quote: the law of contradiction is the most certain of all principles and the basis of logic

Quote: Boole used the symbol 'v' instead of the universal qualifier; e.g., y=vx for \forall y x [»boolG_1854, OK]

Quote: use x=1 for proposition X is true; x=0 for falsehood; xy=1 for proposition X and Y are true together; etc. [»boolG_1854, OK]

Quote: Boole reduced Aristotle's syllogisms and conversions to symbolic logic; scholastic logic is a collection of truths, not a foundation [»boolG_1854, OK]

Quote: Leibniz's work in logic remained unpublished and largely unknown until the turn of the century; Boole, Frege, and Peano may have known of his aims in logic [»leibGW_1686]

Quote: A=A, non-A=non-A, AA=A, non-non-A=A, if A=B then AC=BC for some C, if A=B then non-A=non-B, if A=B then A!=non-B [»leibGW_1686]

Quote: A-non-A is not a thing

Quote: A and A are the first coincidents [»leibGW_1686]

Quote: A and non-A are the first disparities; i.e., it is false that some A is B

Quote: if A is B, it is false that A is non-B

Quote: handle a partially defined predicate by specifying its extension (true for these) and anti-extension (false for these); e.g., three-valued logic [»kripS_1975]

Quote: possible truths are those that do not lead to contradiction; contingent truths lack resolution even if continued to infinity [»leibGW_1686]

Quote: formulas in temporal logic easier to read than first-order logic and decidable; useful for reactive systems; e.g., P will hold eventually [»thomS4_2000]

Quote: SPIN represents correctness claims in linear temporal logic (LTL)

Quote: TRIO--a first-order temporal logic language with a linear notion of time [»ciapE1_1999]

Quote: the TimeLine graphical editor simplifies the specification of basic temporal properties for SPIN model checkers; linear temporal logic is difficult to use [»holzGJ11_2002]

Quote: model checking is automated, symbolic testing for properties expressed in temporal logic; can handle 10^100 states [»thomS4_2000]

Quote: logic model checking is effective for concurrency-related errors; based on temporal logic as proposed by Pnueli [»holzGJ11_2002]

Quote: logic teaches how to know whether or not reasoning is conclusive but it does not teach how to find conclusive reasonings or demonstrations [»galiG_1638]

Quote: logic is not flexible enough for thinking because consistency is too strong a requirement [»minsM_1981]