Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
;; (find-sh "cd ~/books/ && find * | sort")
;; (find-sh "cd ~/books/__logic/ && find * | sort")



;; «.abramsky»			(to "abramsky")
;; «.allwein-barwise»		(to "allwein-barwise")
;; «.andrews»			(to "andrews")
;; «.baader-nipkow»		(to "baader-nipkow")
;; «.barwise»			(to "barwise")
;; «.barwise-etchemendy»	(to "barwise-etchemendy")
;; «.barwise-moss»		(to "barwise-moss")
;; «.bell-machover»		(to "bell-machover")
;; «.bernays»			(to "bernays")
;; «.beziau»			(to "beziau")
;; «.blok-pigozzi»		(to "blok-pigozzi")
;; «.carnap»			(to "carnap")
;; «.carnielli»			(to "carnielli")
;; «.changkeisler»		(to "changkeisler")
;; «.chuaqui»			(to "chuaqui")
;; «.conway»			(to "conway")
;; «.copi»			(to "copi")
;; «.curry»			(to "curry")
;; «.davis»			(to "davis")
;; «.degroote-hindley»		(to "degroote-hindley")
;; «.devlin»			(to "devlin")
;; «.enderton»			(to "enderton")
;; «.fenstadt»			(to "fenstadt")
;; «.fitting»			(to "fitting")
;; «.fraenkel»			(to "fraenkel")
;; «.gabbay»			(to "gabbay")
;; «.gentzen»			(to "gentzen")
;; «.godel»			(to "godel")
;; «.gries-schneider»		(to "gries-schneider")
;; «.henkin»			(to "henkin")
;; «.hindley»			(to "hindley")
;; «.hindley-seldin2»		(to "hindley-seldin2")
;; «.hintikka»			(to "hintikka")
;; «.hofstadter»		(to "hofstadter")
;; «.howard»			(to "howard")
;; «.humberstone»		(to "humberstone")
;; «.hurd»			(to "hurd")
;; «.hurd-loeb»			(to "hurd-loeb")
;; «.jamnik»			(to "jamnik")
;; «.kelley»			(to "kelley")
;; «.kleene»			(to "kleene")
;; «.knuth»			(to "knuth")
;; «.kohlenbach»		(to "kohlenbach")
;; «.kripke»			(to "kripke")
;; «.krivine»			(to "krivine")
;; «.kunen»			(to "kunen")
;; «.landau»			(to "landau")
;; «.luxemburg-robinson»	(to "luxemburg-robinson")
;; «.machover»			(to "machover")
;; «.machover-hirschfeld»	(to "machover-hirschfeld")
;; «.marcos»			(to "marcos")
;; «.martin-lof»		(to "martin-lof")
;; «.mints»			(to "mints")
;; «.mortari»			(to "mortari")
;; «.mortensen»			(to "mortensen")
;; «.nederpelt»			(to "nederpelt")
;; «.nolt-rohatyn»		(to "nolt-rohatyn")
;; «.nordstrom»			(to "nordstrom")
;; «.pohlers»			(to "pohlers")
;; «.prawitz»			(to "prawitz")
;; «.reynolds»			(to "reynolds")
;; «.robinson»			(to "robinson")
;; «.rose-shepherdson»		(to "rose-shepherdson")
;; «.russell»			(to "russell")
;; «.sambin-smith»		(to "sambin-smith")
;; «.saracino-weispfenning»	(to "saracino-weispfenning")
;; «.scheele»			(to "scheele")
;; «.smullyan»			(to "smullyan")
;; «.spencer-brown»		(to "spencer-brown")
;; «.stenlund»			(to "stenlund")
;; «.stroyan»			(to "stroyan")
;; «.stroyan-luxemburg»		(to "stroyan-luxemburg")
;; «.tarski»			(to "tarski")
;; «.tarskiaot»			(to "tarskiaot")
;; «.tarskisclh»		(to "tarskisclh")
;; «.van_dalen»			(to "van_dalen")
;; «.vandenberg-neves»		(to "vandenberg-neves")

;; «.automath»			(to "automath")
;; «.ctt»			(to "ctt")
;; «.games»			(to "games")
;; «.nsa»			(to "nsa")
;; «.tableaux»			(to "tableaux")
;; «.term-rewriting»		(to "term-rewriting")
;; «.typetheory»		(to "typetheory")



;; «abramsky»  (to ".abramsky")
;; http://gigapedia.com/items/124504/handbook-of-logic-in-computer-science-5
(code-djvu       "hlics5" "~/books/__logic/abramsky_gabbay_maibaum__handbook_of_logic_in_computer_science__vol_5.djvu")
(code-djvutotext "hlics5" "~/books/__logic/abramsky_gabbay_maibaum__handbook_of_logic_in_computer_science__vol_5.djvu")
;; (find-hlics5page         9  "Contents")
;; (find-hlics5page (+ 18   1) "Nordstrom")
;; (find-hlics5page (+ 18  39) "Categorical Logic")
;; (find-hlics5page (+ 18  78) "Hyperdoctrines")
;; (find-hlics5text "")


;; «allwein-barwise»  (to ".allwein-barwise")
;; http://gigapedia.com/items/120086/logical-reasoning-with-diagrams--studies-in-logic-and-computation-
(code-xpdf "logreaswithdiags" "~/books/__logic/allwein_barwise__logical_reasoning_with_diagrams.pdf")
;; (find-logreaswithdiagspage        13  "Contents")
;; (find-logreaswithdiagspage (+ 16  49) "Diagrams and the Concept of Logical Systems")
;; (find-logreaswithdiagspage (+ 16  81) "Situation-theoretic Account of Valid Reasoning with Venn Diagrams")
;; (find-logreaswithdiagspage (+ 16 267) "Index")


;; «andrews» (to ".andrews")
;; (find-books "__logic/__logic.el" "andrews")
(code-pdf       "andrewstttp" "~/books/__logic/andrews__an_introduction_to_mathematical_logic_and_type_theory_to_truth_through_proof.pdf")
(code-pdftotext "andrewstttp" "~/books/__logic/andrews__an_introduction_to_mathematical_logic_and_type_theory_to_truth_through_proof.pdf" 13)
;; (find-andrewstttppage)
;; (find-andrewstttppage 6 "Contents")
;; (find-andrewstttptext 6 "Contents")
;; (find-andrewstttppage (+ 13 383) "Index")
;; (find-andrewstttptext (+ 13 383) "Index")
;; (find-andrewstttptext "")




;; «baader-nipkow»  (to ".baader-nipkow")
;; «term-rewriting»  (to ".term-rewriting")
;; http://gigapedia.com/items/329059/term-rewriting-and-all-that
(code-djvu       "termrewrit" "~/books/__logic/baader_nipkow__term_rewriting_and_all_that.djvu")
(code-djvutotext "termrewrit" "~/books/__logic/baader_nipkow__term_rewriting_and_all_that.djvu" 11)
;; (find-termrewritpage         5  "Contents")
;; (find-termrewritpage (+ 11   1) "Chapter 1")
;; (find-termrewritpage (+ 11 278) "A Bluffer's Guide to ML")
;; (find-termrewritpage (+ 11 297) "Index")



;; «barwise»  (to ".barwise")
;; http://gigapedia.com/items/35813/handbook-of-mathematical-logic--studies-in-logic-and-the-foundations-of-mathematics-
(code-djvu       "barwisehandbook" "~/books/__logic/barwise__handbook_of_mathematical_logic.djvu")
(code-djvutotext "barwisehandbook" "~/books/__logic/barwise__handbook_of_mathematical_logic.djvu")
;; (find-barwisehandbookpage        10  "Contents")
;; (find-barwisehandbookpage (+ 12 283) "Kock, Reyes" "Doctrines in Categorical Logic")
;; (find-barwisehandbookpage (+ 12 284)   "only differ in what operations are considered primitve and which derived")
;; (find-barwisehandbookpage (+ 12 289)   "functor ``circle''")
;; (find-barwisehandbookpage (+ 12 305)   "recursive")
;; (find-barwisehandbookpage (+ 12 453) "classes")
;; (find-barwisehandbookpage (+ 12 453) "Devlin" "Constructibility")
;; (find-barwisehandbookpage (+ 12 739) "Aczel" "An introduction to inductive definitions")
;; (find-barwisehandbooktext "")

;; «barwise-etchemendy»  (to ".barwise-etchemendy")
;; http://gigapedia.com/items/29987/language--proof--and-logic
(code-xpdf      "barwiseetchemendy" "~/books/__logic/barwise_etchemendy__language_proof_and_logic.pdf")
(code-pdftotext "barwiseetchemendy" "~/books/__logic/barwise_etchemendy__language_proof_and_logic.pdf" 10)
;; (ee-page-parameters "barwiseetchemendy" 10)
;; (find-barwiseetchemendypage         5  "Contents")
;; (find-barwiseetchemendypage (+ 10  22) "Cube(a)")
;; (find-barwiseetchemendytext (+ 10  22) "Cube(a)")
;; (find-barwiseetchemendypage (+ 10 150) "or-elim")
;; (find-barwiseetchemendypage (+ 10 206) "->-intro")
;; (find-barwiseetchemendypage (+ 10 342) "Fa-elim")
;; (find-barwiseetchemendypage (+ 10 343) "Fa-intro")
;; (find-barwiseetchemendypage (+ 10 347) "Ex-intro")
;; (find-barwiseetchemendypage (+ 10 348) "Ex-elim")
;; (find-barwiseetchemendypage (+ 10 559) "First-order rules")
;; (find-barwiseetchemendypage (+ 10 562) "Glossary")
;; (find-barwiseetchemendypage (+ 10 573) "General Index")
;; (find-barwiseetchemendytext "")

;; trim = function (str) return (str:match "^ *(.-) *$") end
;; redsp = function (str) return (str:gsub(" +", " ")) end
;; PP(trim("  ab cd ef   "))
;; PP(redsp("ab   cd e    f"))
;; titi = function (str) return str:match("^(.-) *([0-9]+)$") end
;; tif = function (tit, p)
;;   if tit then
;;     printf(";; (find-barwiseetchemendypage (+ 10 %3s) \"%s\")\n", p, tit)
;;   end end
;; f = function (str) tif(titi(redsp(trim(str)))) end
;; fs = function (bigstr) for _,li in ipairs(splitlines(bigstr)) do f(li) end end

;; (find-barwiseetchemendypage (+ 10   1) "Introduction")
;; (find-barwiseetchemendypage (+ 10   1)  "The special role of logic in rational inquiry")
;; (find-barwiseetchemendypage (+ 10   2)  "Why learn an artificial language?")
;; (find-barwiseetchemendypage (+ 10   4)  "Consequence and proof")
;; (find-barwiseetchemendypage (+ 10   5)  "Instructions about homework exercises (essential!)")
;; (find-barwiseetchemendypage (+ 10  10)  "To the instructor")
;; (find-barwiseetchemendypage (+ 10  15)  "Web address")
;; (find-barwiseetchemendypage (+ 10  17) "I Propositional Logic")
;; (find-barwiseetchemendypage (+ 10  19) "1 Atomic Sentences")
;; (find-barwiseetchemendypage (+ 10  19)  "1.1 Individual constants")
;; (find-barwiseetchemendypage (+ 10  20)  "1.2 Predicate symbols")
;; (find-barwiseetchemendypage (+ 10  23)  "1.3 Atomic sentences")
;; (find-barwiseetchemendypage (+ 10  28)  "1.4 General first-order languages")
;; (find-barwiseetchemendypage (+ 10  31)  "1.5 Function symbols (optional)")
;; (find-barwiseetchemendypage (+ 10  37)  "1.6 The first-order language of set theory (optional)")
;; (find-barwiseetchemendypage (+ 10  38)  "1.7 The first-order language of arithmetic (optional)")
;; (find-barwiseetchemendypage (+ 10  40)  "1.8 Alternative notation (optional)")
;; (find-barwiseetchemendypage (+ 10  41) "2 The Logic of Atomic Sentences")
;; (find-barwiseetchemendypage (+ 10  41)  "2.1 Valid and sound arguments")
;; (find-barwiseetchemendypage (+ 10  46)  "2.2 Methods of proof")
;; (find-barwiseetchemendypage (+ 10  54)  "2.3 Formal proofs")
;; (find-barwiseetchemendypage (+ 10  58)  "2.4 Constructing proofs in Fitch")
;; (find-barwiseetchemendypage (+ 10  63)  "2.5 Demonstrating nonconsequence")
;; (find-barwiseetchemendypage (+ 10  66)  "2.6 Alternative notation (optional)")
;; (find-barwiseetchemendypage (+ 10  67) "3 The Boolean Connectives")
;; (find-barwiseetchemendypage (+ 10  68)  "3.1 Negation symbol: nt")
;; (find-barwiseetchemendypage (+ 10  71)  "3.2 Conjunction symbol: and")
;; (find-barwiseetchemendypage (+ 10  74)  "3.3 Disjunction symbol: or")
;; (find-barwiseetchemendypage (+ 10  77)  "3.4 Remarks about the game")
;; (find-barwiseetchemendypage (+ 10  79)  "3.5 Ambiguity and parentheses")
;; (find-barwiseetchemendypage (+ 10  82)  "3.6 Equivalent ways of saying things")
;; (find-barwiseetchemendypage (+ 10  84)  "3.7 Translation")
;; (find-barwiseetchemendypage (+ 10  89)  "3.8 Alternative notation (optional)")
;; (find-barwiseetchemendypage (+ 10  93) "4 The Logic of Boolean Connectives")
;; (find-barwiseetchemendypage (+ 10  94)  "4.1 Tautologies and logical truth")
;; (find-barwiseetchemendypage (+ 10 106)  "4.2 Logical and tautological equivalence")
;; (find-barwiseetchemendypage (+ 10 110)  "4.3 Logical and tautological consequence")
;; (find-barwiseetchemendypage (+ 10 114)  "4.4 Tautological consequence in Fitch")
;; (find-barwiseetchemendypage (+ 10 117)  "4.5 Pushing negation around (optional)")
;; (find-barwiseetchemendypage (+ 10 121)  "4.6 Conjunctive and disjunctive normal forms (optional)")
;; (find-barwiseetchemendypage (+ 10 127) "5 Methods of Proof for Boolean Logic")
;; (find-barwiseetchemendypage (+ 10 128)  "5.1 Valid inference steps")
;; (find-barwiseetchemendypage (+ 10 131)  "5.2 Proof by cases")
;; (find-barwiseetchemendypage (+ 10 136)  "5.3 Indirect proof: proof by contradiction")
;; (find-barwiseetchemendypage (+ 10 140)  "5.4 Arguments with inconsistent premises (optional)")
;; (find-barwiseetchemendypage (+ 10 142) "6 Formal Proofs and Boolean Logic")
;; (find-barwiseetchemendypage (+ 10 143)  "6.1 Conjunction rules")
;; (find-barwiseetchemendypage (+ 10 148)  "6.2 Disjunction rules")
;; (find-barwiseetchemendypage (+ 10 154)  "6.3 Negation rules")
;; (find-barwiseetchemendypage (+ 10 163)  "6.4 The proper use of subproofs")
;; (find-barwiseetchemendypage (+ 10 167)  "6.5 Strategy and tactics")
;; (find-barwiseetchemendypage (+ 10 173)  "6.6 Proofs without premises (optional)")
;; (find-barwiseetchemendypage (+ 10 176) "7 Conditionals")
;; (find-barwiseetchemendypage (+ 10 178)  "7.1 Material conditional symbol: ->")
;; (find-barwiseetchemendypage (+ 10 181)  "7.2 Biconditional symbol: <->")
;; (find-barwiseetchemendypage (+ 10 187)  "7.3 Conversational implicature")
;; (find-barwiseetchemendypage (+ 10 190)  "7.4 Truth-functional completeness (optional)")
;; (find-barwiseetchemendypage (+ 10 196)  "7.5 Alternative notation (optional)")
;; (find-barwiseetchemendypage (+ 10 198) "8 The Logic of Conditionals")
;; (find-barwiseetchemendypage (+ 10 198)  "8.1 Informal methods of proof")
;; (find-barwiseetchemendypage (+ 10 206)  "8.2 Formal rules of proof for -> and <->")
;; (find-barwiseetchemendypage (+ 10 214)  "8.3 Soundness and completeness (optional)")
;; (find-barwiseetchemendypage (+ 10 222)  "8.4 Valid arguments: some review exercises")
;; (find-barwiseetchemendypage (+ 10 225) "II Quantifiers")
;; (find-barwiseetchemendypage (+ 10 227) "9 Introduction to Quantification")
;; (find-barwiseetchemendypage (+ 10 228)  "9.1 Variables and atomic wffs")
;; (find-barwiseetchemendypage (+ 10 230)  "9.2 The quantifier symbols: Fa, Ex")
;; (find-barwiseetchemendypage (+ 10 231)  "9.3 Wffs and sentences")
;; (find-barwiseetchemendypage (+ 10 234)  "9.4 Semantics for the quantifiers")
;; (find-barwiseetchemendypage (+ 10 239)  "9.5 The four Aristotelian forms")
;; (find-barwiseetchemendypage (+ 10 243)  "9.6 Translating complex noun phrases")
;; (find-barwiseetchemendypage (+ 10 251)  "9.7 Quantifiers and function symbols (optional)")
;; (find-barwiseetchemendypage (+ 10 255)  "9.8 Alternative notation (optional)")
;; (find-barwiseetchemendypage (+ 10 257) "10 The Logic of Quantifiers")
;; (find-barwiseetchemendypage (+ 10 257)  "10.1 Tautologies and quantification")
;; (find-barwiseetchemendypage (+ 10 266)  "10.2 First-order validity and consequence")
;; (find-barwiseetchemendypage (+ 10 275)  "10.3 First-order equivalence and DeMorgan s laws")
;; (find-barwiseetchemendypage (+ 10 280)  "10.4 Other quantifier equivalences (optional)")
;; (find-barwiseetchemendypage (+ 10 283)  "10.5 The axiomatic method (optional)")
;; (find-barwiseetchemendypage (+ 10 289) "11 Multiple Quantifiers")
;; (find-barwiseetchemendypage (+ 10 289)  "11.1 Multiple uses of a single quantifier")
;; (find-barwiseetchemendypage (+ 10 293)  "11.2 Mixed quantifiers")
;; (find-barwiseetchemendypage (+ 10 298)  "11.3 The step-by-step method of translation")
;; (find-barwiseetchemendypage (+ 10 300)  "11.4 Paraphrasing English")
;; (find-barwiseetchemendypage (+ 10 304)  "11.5 Ambiguity and context sensitivity")
;; (find-barwiseetchemendypage (+ 10 308)  "11.6 Translations using function symbols (optional)")
;; (find-barwiseetchemendypage (+ 10 311)  "11.7 Prenex form (optional)")
;; (find-barwiseetchemendypage (+ 10 315)  "11.8 Some extra translation problems")
;; (find-barwiseetchemendypage (+ 10 319) "12 Methods of Proof for Quantifiers")
;; (find-barwiseetchemendypage (+ 10 319)  "12.1 Valid quantifier steps")
;; (find-barwiseetchemendypage (+ 10 322)  "12.2 The method of existential instantiation")
;; (find-barwiseetchemendypage (+ 10 323)  "12.3 The method of general conditional proof")
;; (find-barwiseetchemendypage (+ 10 329)  "12.4 Proofs involving mixed quantifiers")
;; (find-barwiseetchemendypage (+ 10 338)  "12.5 Axiomatizing shape (optional)")
;; (find-barwiseetchemendypage (+ 10 342) "13 Formal Proofs and Quantifiers")
;; (find-barwiseetchemendypage (+ 10 342)  "13.1 Universal quantifier rules")
;; (find-barwiseetchemendypage (+ 10 347)  "13.2 Existential quantifier rules")
;; (find-barwiseetchemendypage (+ 10 352)  "13.3 Strategy and tactics")
;; (find-barwiseetchemendypage (+ 10 361)  "13.4 Soundness and completeness (optional)")
;; (find-barwiseetchemendypage (+ 10 361)  "13.5 Some review exercises (optional)")
;; (find-barwiseetchemendypage (+ 10 364) "14 More about Quantification (optional)")
;; (find-barwiseetchemendypage (+ 10 366)  "14.1 Numerical quantification")
;; (find-barwiseetchemendypage (+ 10 374)  "14.2 Proving numerical claims")
;; (find-barwiseetchemendypage (+ 10 379)  "14.3 The, both, and neither")
;; (find-barwiseetchemendypage (+ 10 383)  "14.4 Adding other determiners to fol")
;; (find-barwiseetchemendypage (+ 10 389)  "14.5 The logic of generalized quantification")
;; (find-barwiseetchemendypage (+ 10 397)  "14.6 Other expressive limitations of first-order logic")
;; (find-barwiseetchemendypage (+ 10 403) "III Applications and Metatheory")
;; (find-barwiseetchemendypage (+ 10 405) "15 First-order Set Theory")
;; (find-barwiseetchemendypage (+ 10 406)  "15.1 Naive set theory")
;; (find-barwiseetchemendypage (+ 10 412)  "15.2 Singletons, the empty set, subsets")
;; (find-barwiseetchemendypage (+ 10 415)  "15.3 Intersection and union")
;; (find-barwiseetchemendypage (+ 10 419)  "15.4 Sets of sets")
;; (find-barwiseetchemendypage (+ 10 422)  "15.5 Modeling relations in set theory")
;; (find-barwiseetchemendypage (+ 10 427)  "15.6 Functions")
;; (find-barwiseetchemendypage (+ 10 429)  "15.7 The powerset of a set (optional)")
;; (find-barwiseetchemendypage (+ 10 432)  "15.8 Russell s Paradox (optional)")
;; (find-barwiseetchemendypage (+ 10 433)  "15.9 Zermelo Frankel set theory zfc (optional)")
;; (find-barwiseetchemendypage (+ 10 442) "16 Mathematical Induction")
;; (find-barwiseetchemendypage (+ 10 443)  "16.1 Inductive definitions and inductive proofs")
;; (find-barwiseetchemendypage (+ 10 451)  "16.2 Inductive definitions in set theory")
;; (find-barwiseetchemendypage (+ 10 453)  "16.3 Induction on the natural numbers")
;; (find-barwiseetchemendypage (+ 10 456)  "16.4 Axiomatizing the natural numbers (optional)")
;; (find-barwiseetchemendypage (+ 10 458)  "16.5 Proving programs correct (optional)")
;; (find-barwiseetchemendypage (+ 10 468) "17 Advanced Topics in Propositional Logic")
;; (find-barwiseetchemendypage (+ 10 468)  "17.1 Truth assignments and truth tables")
;; (find-barwiseetchemendypage (+ 10 470)  "17.2 Completeness for propositional logic")
;; (find-barwiseetchemendypage (+ 10 479)  "17.3 Horn sentences (optional)")
;; (find-barwiseetchemendypage (+ 10 488)  "17.4 Resolution (optional)")
;; (find-barwiseetchemendypage (+ 10 495) "18 Advanced Topics in FOL")
;; (find-barwiseetchemendypage (+ 10 495)  "18.1 First-order structures")
;; (find-barwiseetchemendypage (+ 10 500)  "18.2 Truth and satisfaction, revisited")
;; (find-barwiseetchemendypage (+ 10 509)  "18.3 Soundness for fol")
;; (find-barwiseetchemendypage (+ 10 512)  "18.4 The completeness of the shape axioms (optional)")
;; (find-barwiseetchemendypage (+ 10 514)  "18.5 Skolemization (optional)")
;; (find-barwiseetchemendypage (+ 10 516)  "18.6 Unification of terms (optional)")
;; (find-barwiseetchemendypage (+ 10 519)  "18.7 Resolution, revisited (optional)")
;; (find-barwiseetchemendypage (+ 10 526) "19 Completeness and Incompleteness")
;; (find-barwiseetchemendypage (+ 10 527)  "19.1 The Completeness Theorem for fol")
;; (find-barwiseetchemendypage (+ 10 529)  "19.2 Adding witnessing constants")
;; (find-barwiseetchemendypage (+ 10 531)  "19.3 The Henkin theory")
;; (find-barwiseetchemendypage (+ 10 534)  "19.4 The Elimination Theorem")
;; (find-barwiseetchemendypage (+ 10 540)  "19.5 The Henkin Construction")
;; (find-barwiseetchemendypage (+ 10 546)  "19.6 The Lowenheim-Skolem Theorem")
;; (find-barwiseetchemendypage (+ 10 548)  "19.7 The Compactness Theorem")
;; (find-barwiseetchemendypage (+ 10 552)  "19.8 The Godel Incompleteness Theorem")
;; (find-barwiseetchemendypage (+ 10 557) "Summary of Formal Proof Rules")
;; (find-barwiseetchemendypage (+ 10 557) "Propositional rules")
;; (find-barwiseetchemendypage (+ 10 559) "First-order rules")
;; (find-barwiseetchemendypage (+ 10 561) "Inference Procedures (Con Rules)")
;; (find-barwiseetchemendypage (+ 10 562) "Glossary")
;; (find-barwiseetchemendypage (+ 10 573) "General Index")
;; (find-barwiseetchemendypage (+ 10 585) "Exercise Files Index")


;; «barwise-moss»  (to ".barwise-moss")
;; http://gigapedia.org/items/47442/vicious-circles--center-for-the-study-of-language-and-information---lecture-notes-
(code-djvu "viccircles" "~/books/__logic/barwise_moss__vicious_circles.djvu")
;; (find-viccirclespage         7  "Contents")
;; (find-viccirclespage (+ 10 385) "Index")


;; «bell-machover»  (to ".bell-machover")
(code-djvu       "bellmachover" "~/books/__logic/bell_machover__a_course_in_mathematical_logic.djvu")
(code-djvutotext "bellmachover" "~/books/__logic/bell_machover__a_course_in_mathematical_logic.djvu")
;; (find-bellmachoverpage         8  "Contents")
;; (find-bellmachoverpage (+ 18 585) "Index")
;; (find-bellmachovertext "")


;; «bernays»  (to ".bernays")
(code-djvu "scowbernays" "~/books/__logic/mueller__sets_and_classes_on_the_work_of_paul_bernays.djvu")
;; (find-scowbernayspage         1  "Contents")
;; (find-scowbernayspage (+ 19   1) "1")
;; (find-scowbernayspage (+ 14 353) "Index")



;; «beziau»  (to ".beziau")
;; http://gigapedia.com/items/51559/logica-universalis--towards-a-general-theory-of-logic
;; http://gigapedia.com/items/70500/logica-universalis--towards-a-general-theory-of-logic-2nd-ed
(code-xpdf "logicauniversalis" "~/books/__logic/beziau__logica_universalis_towards_a_general_theory_of_logic.pdf")
;; (find-logicauniversalispage         5  "Contents")
;; (find-logicauniversalispage (+ -1 169) "The humbug of many logical values")




;; «blok-pigozzi» (to ".blok-pigozzi")
;; (find-books "__logic/__logic.el" "blok-pigozzi")
(code-pdf       "blokpig" "~/books/__logic/blok_pigozzi__algebraizable_logics.pdf")
(code-pdftotext "blokpig" "~/books/__logic/blok_pigozzi__algebraizable_logics.pdf" 1)
;; (find-blokpigpage)
;; (find-blokpigpage        1  "Contents")
;; (find-blokpigpage (+ 1 189) "Index")
;; (find-blokpigtext "")


;; «carnap» (to ".carnap")
(code-djvu       "carnapprob" "~/books/__logic/carnap__logical_foundations_of_probability.djvu")
(code-djvutotext "carnapprob" "~/books/__logic/carnap__logical_foundations_of_probability.djvu" 25)
;; (find-carnapprobpage)
;; (find-carnapprobpage        21  "Contents")
;; (find-carnapprobpage (+ 17 605) "Index")
;; (find-carnapprobtext "")

;; «carnielli» (to ".carnielli")
;; (find-books "__logic/__logic.el" "carnielli")
(code-pdf       "cacoparalococo" "~/books/__logic/carnielli_coniglio__paraconsistent_logic_consistency_contradiction_and_negation.pdf")
(code-pdftotext "cacoparalococo" "~/books/__logic/carnielli_coniglio__paraconsistent_logic_consistency_contradiction_and_negation.pdf" 1)
;; (find-cacoparalococopage)
;; (find-cacoparalococopage       20  "Contents")
;; (find-cacoparalococopage (+ 1 189) "Index")
;; (find-cacoparalococotext "")


;; «changkeisler»  (to ".changkeisler")
;; http://gigapedia.com/items/155775/model-theory--studies-in-logic-and-the-foundations-of-mathematics-
(code-djvu "changkeisler" "~/books/__logic/chang_keisler__model_theory.djvu")
;; (find-changkeislerpage      1  "Contents")
;; (find-changkeislerpage (+ 1 1) "Index")

;; «chuaqui»  (to ".chuaqui")
(code-djvu "chuaqui" "~/books/__logic/chuaqui__axiomatic_set_theory.djvu")
;; (find-chuaquipage      1  "Contents")
;; (find-chuaquipage (+ 1 1) "Index")

;; «conway»  (to ".conway")
;; http://gigapedia.com/items/67259/on-numbers-and-games--l-m-s--monographs---no--6-
;; http://gigapedia.com/items/20515/the-book-of-numbers
(code-djvu "onag" "~/books/__logic/conway__on_numbers_and_games.djvu")
(code-djvu "bookofnumbers" "~/books/__logic/conway_guy__the_book_of_numbers.djvu")
;; (find-onagpage        9  "Contents")
;; (find-onagpage (+ 5 231) "Index")
;; (find-bookofnumberspage   6  "Contents")
;; (find-bookofnumberspage 301 "Index")

;; «copi» (to ".copi")
;; (find-books "__logic/__logic.el" "copi")
(code-djvu       "copipt" "~/books/__logic/copi__introducao_a_logica.djvu")
(code-djvutotext "copipt" "~/books/__logic/copi__introducao_a_logica.djvu" 1)
;; (find-copiptpage)
;; (find-copiptpage        1  "Contents")
;; (find-copiptpage (+ 3 477) "Index")
;; (find-copipttext "")

(code-pdf       "copien" "~/books/__logic/copi__introduction_to_logic.pdf")
(code-pdftotext "copien" "~/books/__logic/copi__introduction_to_logic.pdf" 1)
;; (find-copienpage)
;; (find-copienpage        1  "Contents")
;; (find-copienpage (+ 1 189) "Index")
;; (find-copientext "")


;; «curry»  (to ".curry")
;; http://gigapedia.com/items/126830/foundations-of-mathematical-logic
;; http://gigapedia.com/items/259486/combinatory-logic--volumes-i-and-ii--studies-in-logic-and-the-foundations-of-mathematics-
(code-djvu "curryfound" "~/books/__logic/curry__foundations_of_mathematical_logic.djvu")
;; (find-curryfoundpage        7  "Contents")
;; (find-curryfoundpage (+ 9 391) "Index")
(code-djvu "curryfeys1" "~/books/__logic/curry_feys__combinatory_logic_vol_1.djvu")
;; (find-curryfeys1page      1  "Contents")
;; (find-curryfeys1page (+ 7 397) "Index")

;; «davis»  (to ".davis")
;; http://gigapedia.com/items/135960/engines-of-logic--or-the-universal-computer---mathematicians-and-the-origin-of-the-computer
(code-djvu "enginesoflogic" "~/books/__logic/davis__engines_of_logic.djvu")
;; (find-enginesoflogicpage         6  "Contents")
;; (find-enginesoflogicpage (+ 11 249) "Index")

;; «degroote-hindley»  (to ".degroote-hindley")
;; http://gigapedia.com/items/114823/typed-lambda-calculi-and-applications--third-international-conference-on-typed-lambda-calculi-and-applications--tlca---039-97--nancy--france--april-2-4--1997-------lecture-notes-in-computer-science-
(code-xpdf "tlca97" "~/books/__logic/de_groote_hindley__tlca_97.pdf")
;; (find-tlca97page        6  "Contents")
;; (find-tlca97page (+ 7  82) "Torben Brauner" "A simple adequate categorical model for PCF")
;; (find-tlca97page (+ 7 164) "Neil Ghani" "Eta-expansions in Dependent Type Theory")
;; (find-tlca97page (+ 7 181) "Martini/Masini")
;; (find-tlca97page (+ 7 354) "Takeuti, Izumi" "An Axiomatic System of Parametricity")
;; (find-tlca97page (+ 7 373) "Urzyczyn")

;; «devlin»  (to ".devlin")
;; http://gigapedia.com/items/119048/the-joy-of-sets--fundamentals-of-contemporary-set-theory--undergraduate-texts-in-mathematics---second-edition
(code-djvu "devlin" "~/books/__logic/devlin__the_joy_of_sets.djvu")
;; (find-devlinpage        10  "Contents")
;; (find-devlinpage (+ 11 189) "Index")

;; «enderton»  (to ".enderton")
;; http://www.math.ucla.edu/~hbe/amil/
;; http://gigapedia.com/items/35707/a-mathematical-introduction-to-logic--2nd-edition
;; http://gigapedia.com/items/10671/elements-of-set-theory
(code-djvu "enderton"   "~/books/__logic/enderton__a_mathematical_introduction_to_logic.djvu")
(code-djvu "endertonst" "~/books/__logic/enderton__elements_of_set_theory.djvu")
;; (find-endertonpage        4  "Contents")
;; (find-endertonpage (+ 9 311) "Index")
;; (find-endertonstpage         4  "Contents")
;; (find-endertonstpage (+ 10 273) "Index")

;; «fenstadt»  (to ".fenstadt")
;; http://gigapedia.com/items/124942/introduction-to-metamathematics--bibliotheca-mathematica---bibliotheca-mathematica-
;; http://gigapedia.com/items/259363/proceedings-of-the-second-scandinavian-logic-symposium--studies-in-logic-and-the-foundations-of-mathematics-
(code-xpdf "2ndscandlogsymp" "~/books/__logic/fenstad_ed__proceedings_of_the_second_scandinavian_logic_symposium.pdf")
;; (find-2ndscandlogsymppage (+  4   1) "On the decision problems...")
;; (find-2ndscandlogsymppage (+  1   1) "Index")
;; (find-2ndscandlogsymppage (+  3  63) "Girard")
;; (find-2ndscandlogsymppage (+  3 179) "Martin-Löf")
;; (find-2ndscandlogsymppage (+  2 217) "Martin-Löf")
;; (find-2ndscandlogsymppage (+  1 235) "Prawitz")
;; (find-2ndscandlogsymppage (+  0 309) "Quine")
;; (find-2ndscandlogsymppage (+ -2 369) "Troelstra")

;; «fitting»  (to ".fitting")
;; http://gigapedia.com/items/255507/intuitionistic-logic--model-theory-and-forcing--studies-in-logic-and-the-foundations-of-mathematics-
(code-xpdf "fittingforcing" "~/books/__logic/fitting__intuitionistic_logic_model_theory_and_forcing.pdf")
;; (find-fittingforcingpage          8  "Chapter 1")
;; (find-fittingforcingpage (+ -14 190) "Index")

;; «fraenkel»  (to ".fraenkel")
;; http://gigapedia.com/items/255513/abstract-set-theory--studies-in-logic-and-the-foundations-of-mathematics-
(code-xpdf "fraenkelast" "~/books/__logic/fraenkel__abstract_set_theory.pdf")
;; (find-fraenkelastpage      1  "Contents")
;; (find-fraenkelastpage (+ 1 1) "Index")

;; «gabbay»  (to ".gabbay")
;; http://gigapedia.com/items/120096/labelled-deductive-systems--volume-1--oxford-logic-guides-
(code-djvu       "gabbaylds1" "~/books/__logic/gabbay__labelled_deductive_systems_vol_1.djvu")
(code-djvutotext "gabbaylds1" "~/books/__logic/gabbay__labelled_deductive_systems_vol_1.djvu")
;; (find-gabbaylds1page        11  "Contents")
;; (find-gabbaylds1page (+ 14   1) "1. What is a logical system?")
;; (find-gabbaylds1page (+ 14  10) "Surgical cut")
;; (find-gabbaylds1page (+ 14 141) "3. Introducing Algebraic Labelled Deductive Systems")
;; (find-gabbaylds1page (+ 14 159) "Diagram rule")
;; (find-gabbaylds1page (+ 14 160) "Quantifier elimination and introduction rules")
;; (find-gabbaylds1page (+ 14 161) "proof from a database")
;; (find-gabbaylds1page (+ 14 176) "3.3. Introduction rules: a discussion")
;; (find-gabbaylds1page (+ 14 198) "3.5. The metabox system")
;; (find-gabbaylds1page (+ 14 251) "defeasible")
;; (find-gabbaylds1page (+ 14 321) "Micro-PROLOG")
;; (find-gabbaylds1page (+ 14 323) "6.5. Metalevel features via connectives")
;; (find-gabbaylds1page (+ 14 375) "8. Extending the Curry-Howard Interpretation to LDS Systems")
;; (find-gabbaylds1page (+ 14 493) "Index")
;; (find-gabbaylds1text "")

;; (find-books "__logic/__logic.el" "gabbay")
(code-pdf       "siihil" "~/books/__logic/gabbay__semantical_investigations_in_heytings_intuitionistic_logic.pdf")
(code-pdftotext "siihil" "~/books/__logic/gabbay__semantical_investigations_in_heytings_intuitionistic_logic.pdf" 10)
;; (find-siihilpage)
;; (find-siihilpage         7  "Contents")
;; (find-siihilpage (+ 10   1) "Introduction")
;; (find-siihilpage (+ 10 285) "Index")
;; (find-siihiltext "")


;; «gentzen»  (to ".gentzen")
;; http://gigapedia.org/items/210120/the-collected-papers-of-gerhard-gentzen--north-holland-1969---ed--m-e-szabo-
(code-djvu "gentzenpapers" "~/books/__logic/gentzen__the_collected_papers.djvu")
;; (find-gentzenpaperspage         7  "Contents")
;; (find-gentzenpaperspage (+ 12  68) "Investigations into logical deduction")
;; (find-gentzenpaperspage (+ 12 324) "Index of subjects")

;; «godel» (to ".godel")
;; (find-books "__logic/__logic.el" "godel")
;; (find-LATEX "catsem.bib" "bib-Goedel")
(code-pdf       "godel1" "~/books/__logic/godel___collected_works_1.pdf")
(code-pdftotext "godel1" "~/books/__logic/godel___collected_works_1.pdf" 27)
(code-pdf       "godel2" "~/books/__logic/godel___collected_works_2.pdf")
(code-pdftotext "godel2" "~/books/__logic/godel___collected_works_2.pdf" 19)
;; (find-godel1page)
;; (find-godel1page        18  "Contents")
;; (find-godel1page (+ 27  16) "Works in the first two volumes")
;; (find-godel1page (+ 27 223) "On the intuitionistic propositional calculus")
;; (find-godel1page (+ 27 296) "Introductory note to 1933f")
;; (find-godel1page (+ 27 301) "An interpretation of the intuitionistic propositional calculus (1933f)")
;; (find-godel1page (+ 27 461) "Index")
;; (find-godel1text "")
;; (find-godel2page)
;; (find-godel2page        14  "Contents")
;; (find-godel2page (+ 19   1) "Index")
;; (find-godel2page (+ 19 393) "Index")
;; (find-godel2text "")


;; «gries-schneider»  (to ".gries-schneider")
(code-xpdf      "griesschneider" "~/books/__logic/gries_schneider__a_logical_approach_to_discrete_math.pdf")
(code-pdftotext "griesschneider" "~/books/__logic/gries_schneider__a_logical_approach_to_discrete_math.pdf")
;; (find-griesschneiderpage      1  "Contents")
;; (find-griesschneiderpage (+ 1 1) "Index")
;; (find-griesschneidertext "")


;; «henkin» (to ".henkin")
;; Leon Henkin: The logic of equality (1977)
;; https://www.jstor.org/stable/2321009
;; (find-books "__logic/__logic.el" "henkin")
(code-pdf       "henkinleq" "~/books/__logic/henkin1977.pdf")
(code-pdftotext "henkinleq" "~/books/__logic/henkin1977.pdf" -595)
;; (find-henkinleqpage)
;; (find-henkinleqpage        1  "Contents")
;; (find-henkinleqpage (+ 1 189) "Index")
;; (find-henkinleqpage (+ -595 597))
;; (find-henkinleqtext (+ -595 597))
;; (find-henkinleqtext "")



;; «hindley»  (to ".hindley")
;; (find-books "__logic/__logic.el" "hindley")
(code-pdf       "hindleyseldin2" "~/books/__logic/hindley_seldin__lambda-calculus_and_combinators_2nd_ed.pdf")
(code-pdftotext "hindleyseldin2" "~/books/__logic/hindley_seldin__lambda-calculus_and_combinators_2nd_ed.pdf" 14)
;; (find-hindleyseldin2page)
;; (find-hindleyseldin2page         8  "Contents")
;; (find-hindleyseldin2page (+ 14 107) "10   Simple typing, Church-style")
;; (find-hindleyseldin2page (+ 14 147) "11J Propositions-as-types and normalization")
;; (find-hindleyseldin2page (+ 14 334) "List of symbols")
;; (find-hindleyseldin2page (+ 14 337) "Index")
;; (find-hindleyseldin2text "")

;; «hindley-seldin2» (to ".hindley-seldin2")
;; (find-books "__logic/__logic.el" "hindley-seldin2")
(code-pdf       "hindleyseldin2" "~/books/__logic/hindley_seldin__lambda-calculus_and_combinators_an_introduction.pdf")
(code-pdftotext "hindleyseldin2" "~/books/__logic/hindley_seldin__lambda-calculus_and_combinators_an_introduction.pdf" 14)
;; (find-hindleyseldin2page)
;; (find-hindleyseldin2page        1  "Contents")
;; (find-hindleyseldin2page (+ 1 189) "Index")
;; (find-hindleyseldin2text "")

;; (find-hindleyseldin2page (+ 14   1)  "1  The -calculus")
;; (find-hindleyseldin2page (+ 14   1)  "1A Introduction")
;; (find-hindleyseldin2page (+ 14   5)  "1B Term-structure and substitution")
;; (find-hindleyseldin2page (+ 14  11)  "1C -reduction")
;; (find-hindleyseldin2page (+ 14  16)  "1D -equality")
;; (find-hindleyseldin2page (+ 14  21)  "2  Combinatory logic")
;; (find-hindleyseldin2page (+ 14  21)  "2A Introduction to CL")
;; (find-hindleyseldin2page (+ 14  24)  "2B Weak reduction")
;; (find-hindleyseldin2page (+ 14  26)  "2C Abstraction in CL")
;; (find-hindleyseldin2page (+ 14  29)  "2D Weak equality")
;; (find-hindleyseldin2page (+ 14  33)  "3  The power of and combinators")
;; (find-hindleyseldin2page (+ 14  33)  "3A Introduction")
;; (find-hindleyseldin2page (+ 14  34)  "3B The fixed-point theorem")
;; (find-hindleyseldin2page (+ 14  36)  "3C B¨ohm's theorem")
;; (find-hindleyseldin2page (+ 14  40)  "3D The quasi-leftmost-reduction theorem")
;; (find-hindleyseldin2page (+ 14  43)  "3E History and interpretation")
;; (find-hindleyseldin2page (+ 14  47)  "4  Representing the computable functions")
;; (find-hindleyseldin2page (+ 14  47)  "4A Introduction")
;; (find-hindleyseldin2page (+ 14  50)  "4B Primitive recursive functions")
;; (find-hindleyseldin2page (+ 14  56)  "4C Recursive functions")
;; (find-hindleyseldin2page (+ 14  61)  "4D Abstract numerals and Z")
;; (find-hindleyseldin2page (+ 14  63)  "5  The undecidability theorem")
;; (find-hindleyseldin2page (+ 14  69)  "6  The formal theories and CLw")
;; (find-hindleyseldin2page (+ 14  69)  "6A The definitions of the theories")
;; (find-hindleyseldin2page (+ 14  72)  "6B First-order theories")
;; (find-hindleyseldin2page (+ 14  73)  "6C Equivalence of theories")
;; (find-hindleyseldin2page (+ 14  76)  "7  Extensionality in -calculus")
;; (find-hindleyseldin2page (+ 14  76)  "7A Extensional equality")
;; (find-hindleyseldin2page (+ 14  79)  "7B -reduction in -calculus")
;; (find-hindleyseldin2page (+ 14  82)  "8  Extensionality in combinatory logic")
;; (find-hindleyseldin2page (+ 14  82)  "8A Extensional equality")
;; (find-hindleyseldin2page (+ 14  85)  "8B Axioms for extensionality in CL")
;; (find-hindleyseldin2page (+ 14  89)  "8C Strong reduction")
;; (find-hindleyseldin2page (+ 14  92)  "9  Correspondence between and CL")
;; (find-hindleyseldin2page (+ 14  92)  "9A Introduction")
;; (find-hindleyseldin2page (+ 14  95)  "9B The extensional equalities")
;; (find-hindleyseldin2page (+ 14 100)  "9C New abstraction algorithms in CL")
;; (find-hindleyseldin2page (+ 14 102)  "9D Combinatory -equality")
;; (find-hindleyseldin2page (+ 14 107) "10  Simple typing, Church-style")
;; (find-hindleyseldin2page (+ 14 107) "10A Simple types")
;; (find-hindleyseldin2page (+ 14 109) "10B Typed -calculus")
;; (find-hindleyseldin2page (+ 14 115) "10C Typed CL")
;; (find-hindleyseldin2page (+ 14 119) "11  Simple typing, Curry-style in CL")
;; (find-hindleyseldin2page (+ 14 119) "11A Introduction")
;; (find-hindleyseldin2page (+ 14 122) "11B The system TA C")
;; (find-hindleyseldin2page (+ 14 126) "11C Subject-construction")
;; (find-hindleyseldin2page (+ 14 127) "11D Abstraction")
;; (find-hindleyseldin2page (+ 14 130) "11E Subject-reduction")
;; (find-hindleyseldin2page (+ 14 134) "11F Typable CL-terms")
;; (find-hindleyseldin2page (+ 14 137) "11G Link with Church's approach")
;; (find-hindleyseldin2page (+ 14 138) "11H Principal types")
;; (find-hindleyseldin2page (+ 14 143) "11I Adding new axioms")
;; (find-hindleyseldin2page (+ 14 147) "11J Propositions-as-types and normalization")
;; (find-hindleyseldin2page (+ 14 155) "11K The equality-rule Eq")
;; (find-hindleyseldin2page (+ 14 159) "12  Simple typing, Curry-style in")
;; (find-hindleyseldin2page (+ 14 159) "12A The system TA")
;; (find-hindleyseldin2page (+ 14 165) "12B Basic properties of TA")
;; (find-hindleyseldin2page (+ 14 170) "12C Typable -terms")
;; (find-hindleyseldin2page (+ 14 173) "12D Propositions-as-types and normalization")
;; (find-hindleyseldin2page (+ 14 176) "12E The equality-rule Eq")
;; (find-hindleyseldin2page (+ 14 180) "13  Generalizations of typing")
;; (find-hindleyseldin2page (+ 14 180) "13A Introduction")
;; (find-hindleyseldin2page (+ 14 181) "13B Dependent function types, introduction")
;; (find-hindleyseldin2page (+ 14 183) "13C Basic generalized typing, Curry-style in")
;; (find-hindleyseldin2page (+ 14 187) "13D Deductive rules to define types")
;; (find-hindleyseldin2page (+ 14 191) "13E Church-style typing in")
;; (find-hindleyseldin2page (+ 14 192)     "Definition 13.23 (-cube)")
;; (find-hindleyseldin2text (+ 14 192)     "Definition 13.23 (-cube)")
;; (find-hindleyseldin2page (+ 14 202) "13F Normalization in PTSs")
;; (find-hindleyseldin2page (+ 14 209) "13G Propositions-as-types")
;; (find-hindleyseldin2page (+ 14 217) "13H PTSs with equality")
;; (find-hindleyseldin2page (+ 14 220) "14  Models of CL")
;; (find-hindleyseldin2page (+ 14 220) "14A Applicative structures")
;; (find-hindleyseldin2page (+ 14 223) "14B Combinatory algebras")
;; (find-hindleyseldin2page (+ 14 229) "15  Models of -calculus")
;; (find-hindleyseldin2page (+ 14 229) "15A The definition of -model")
;; (find-hindleyseldin2page (+ 14 236) "15B Syntax-free definitions")
;; (find-hindleyseldin2page (+ 14 242) "15C General properties of -models")
;; (find-hindleyseldin2page (+ 14 247) "16  Scott's D and other models")
;; (find-hindleyseldin2page (+ 14 247) "16A Introduction: complete partial orders")
;; (find-hindleyseldin2page (+ 14 252) "16B Continuous functions")
;; (find-hindleyseldin2page (+ 14 256) "16C The construction of D")
;; (find-hindleyseldin2page (+ 14 261) "16D Basic properties of D")
;; (find-hindleyseldin2page (+ 14 267) "16E D is a -model")
;; (find-hindleyseldin2page (+ 14 271) "16F Some other models")
;; (find-hindleyseldin2page (+ 14 276) "Appendix A1 Bound variables and -conversion")
;; (find-hindleyseldin2page (+ 14 282) "Appendix A2 Confluence proofs")
;; (find-hindleyseldin2page (+ 14 293) "Appendix A3 Strong normalization proofs")
;; (find-hindleyseldin2page (+ 14 305) "Appendix A4 Care of your pet combinator")
;; (find-hindleyseldin2page (+ 14 307) "Appendix A5 Answers to starred exercises")
;; (find-hindleyseldin2page (+ 14 323) "References")
;; (find-hindleyseldin2page (+ 14 334) "List of symbols")
;; (find-hindleyseldin2page (+ 14 337) "Index")
;; (find-hindleyseldin2text )




;; «hintikka»  (to ".hintikka")
;; http://gigapedia.com/items/35756/the-philosophy-of-mathematics--oxford-readings-in-philosophy-
(code-djvu "hintikkaphilmat" "~/books/__logic/hintikka_ed__the_philosophy_of_mathematics.djvu")
;; (find-hintikkaphilmatpage    176     "Contents")
;; (find-hintikkaphilmatpage (+ 176  1) "Introduction")
;; (find-hintikkaphilmatpage (+ 176  9) "I. Semantic entailment and formal derivability" "E.W. Beth")
;; (find-hintikkaphilmatpage (+ -12 14) "I. 3. Heuristic considerations")
;; (find-hintikkaphilmatpage (+ -12 42) "II. The completeness of the first-order functional calculus" "Leon Henkin")
;; (find-hintikkaphilmatpage (+ -12 95) "VI. Systems of predicative analysis" "Solomon Feferman")

;; «hofstadter»  (to ".hofstadter")
(code-xpdf      "geb" "~/books/__logic/hofstadter__godel_escher_bach_an_eternal_golden_braid.pdf")
(code-pdftotext "geb" "~/books/__logic/hofstadter__godel_escher_bach_an_eternal_golden_braid.pdf" 0)
;; (ee-page-parameters "geb" 0)
;; (find-gebpage        1  "Contents")
;; (find-gebpage 193 "The Converse of the Fantasy Rule")
;; (find-gebtext 193 "The Converse of the Fantasy Rule")
;; (find-gebpage (+ 9 761) "Index")
;; (find-gebtext "")


;; «howard» (to ".howard")
;; https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf
;; (find-fline "$S/https/www.cs.cmu.edu/~crary/819-f09/")
(code-xpdf     "howard80" "$S/https/www.cs.cmu.edu/~crary/819-f09/Howard80.pdf")
(code-pdf-text "howard80" "$S/https/www.cs.cmu.edu/~crary/819-f09/Howard80.pdf" -479)
;; (find-howard80page)
;; (find-howard80text)
;; (find-howard80page (+ -479 480))


;; «humberstone» (to ".humberstone")
;; (find-books "__logic/__logic.el" "humberstone")
(code-pdf       "connectives" "~/books/__logic/humberstone__the_connectives.pdf")
(code-pdftotext "connectives" "~/books/__logic/humberstone__the_connectives.pdf" 19)
;; (find-connectivespage)
;; (find-connectivespage          8  "Contents")
;; (find-connectivespage         14  "Preface")
;; (find-connectivespage (+ 19    1) "0. Preliminaries")
;; (find-connectivespage (+ 19   47) "1 Elements of Sentential Logic")
;; (find-connectivespage (+ 19   47) "1.1 TRUTH AND CONSEQUENCE")
;; (find-connectivespage (+ 19   47) "1.11 Languages")
;; (find-connectivespage (+ 19   54) "1.12 Consequence Relations and Valuations")
;; (find-connectivespage (+ 19   61) "1.13 #-Classical Consequence Relations and #-Boolean Valuations")
;; (find-connectivespage (+ 19   67) "1.14 Forcing Consistent Valuations to Be #-Boolean")
;; (find-connectivespage (+ 19   72) "1.15 Two Equations and the `Converse Proposition' Fallacy")
;; (find-connectivespage (+ 19   73) "1.16 Generalized Consequence Relations")
;; (find-connectivespage (+ 19   79) "1.17 Generalized Consequence Relations: Supplementary Discussion")
;; (find-connectivespage (+ 19   82) "1.18 Truth-Tables, and Two More Connectives: Implication and Equivalence")
;; (find-connectivespage (+ 19   87) "1.19 A More Hygienic Terminology")
;; (find-connectivespage (+ 19  100) "Notes and References for §1.1")
;; (find-connectivespage (+ 19  103) "1.2 RULES AND PROOF")
;; (find-connectivespage (+ 19  103) "1.21 Sequents and Frameworks")
;; (find-connectivespage (+ 19  112) "1.22 Sequents and (Generalized) Consequence Relations")
;; (find-connectivespage (+ 19  114) "1.23 A Sample Natural Deduction System in Set-Fmla")
;; (find-connectivespage (+ 19  122) "1.24 A Closer Look at Rules")
;; (find-connectivespage (+ 19  127) "1.25 Semantic Apparatus for Sequents and for Rules")
;; (find-connectivespage (+ 19  132) "1.26 Two Relational Connections")
;; (find-connectivespage (+ 19  140) "1.27 Sample Natural Deduction and Sequent Calculus Systems in Set-Set")
;; (find-connectivespage (+ 19  150) "1.28 Some Other Approaches to Logic in Set-Set")
;; (find-connectivespage (+ 19  156) "1.29 Axiom Systems and the Deduction Theorem")
;; (find-connectivespage (+ 19  180) "Appendix to §1.2: What Is a Logic?")
;; (find-connectivespage (+ 19  188) "Notes and References for §1.2")
;; (find-connectivespage (+ 19  195) "2 A Survey of Sentential Logic")
;; (find-connectivespage (+ 19  195) "2.1 MANY-VALUED LOGIC AND ALGEBRAIC SEMANTICS")
;; (find-connectivespage (+ 19  195) "2.11 Many-Valued Logic: Matrices")
;; (find-connectivespage (+ 19  211) "2.12 Many-Valued Logic: Classes of Matrices")
;; (find-connectivespage (+ 19  219) "2.13 Algebraic Semantics: Matrices with a Single Designated Value")
;; (find-connectivespage (+ 19  246) "2.14 -Based Algebraic Semantics")
;; (find-connectivespage (+ 19  250) "2.15 A Third Version of Algebraic Semantics: Indiscriminate Validity")
;; (find-connectivespage (+ 19  257) "2.16 From Algebraic Semantics to Equivalent Algebraic Semantics")
;; (find-connectivespage (+ 19  268) "Notes and References for §2.1")
;; (find-connectivespage (+ 19  275) "2.2 MODAL LOGIC")
;; (find-connectivespage (+ 19  275) "2.21 Modal Logic in Fmla: Introduction")
;; (find-connectivespage (+ 19  282) "2.22 Modal Logic in Fmla: Kripke Frames.")
;; (find-connectivespage (+ 19  288) "2.23 Other Logical Frameworks")
;; (find-connectivespage (+ 19  296) "Notes and References for §2.2")
;; (find-connectivespage (+ 19  298) "2.3 THREE RIVALS TO CLASSICAL LOGIC")
;; (find-connectivespage (+ 19  298) "2.31 Quantum Logic")
;; (find-connectivespage (+ 19  302) "2.32 Intuitionistic Logic")
;; (find-connectivespage (+ 19  326) "2.33 Relevant and Linear Logic")
;; (find-connectivespage (+ 19  369) "Notes and References for §2.3")
;; (find-connectivespage (+ 19  375) "3 Connectives: Truth-Functional, Extensional, Congruential")
;; (find-connectivespage (+ 19  375) "3.1 TRUTH-FUNCTIONALITY")
;; (find-connectivespage (+ 19  375) "3.11 Truth-Functional Connectives")
;; (find-connectivespage (+ 19  382) "3.12 Pathologies of Overdetermination")
;; (find-connectivespage (+ 19  385) "3.13 Determinant-induced Conditions on a Consequence Relation")
;; (find-connectivespage (+ 19  403) "3.14 Functional Completeness, Duality, and Dependence")
;; (find-connectivespage (+ 19  418) "3.15 Definability of Connectives")
;; (find-connectivespage (+ 19  423) "3.16 Defining a Connective")
;; (find-connectivespage (+ 19  428) "3.17 Truth-Functions, Rules, and Matrices")
;; (find-connectivespage (+ 19  436) "3.18 Intuitionistically Dangerous Determinants")
;; (find-connectivespage (+ 19  442) "Notes and References for §3.1")
;; (find-connectivespage (+ 19  444) "3.2 EXTENSIONALITY")
;; (find-connectivespage (+ 19  444) "3.21 A Biconditional-based Introduction to Extensionality")
;; (find-connectivespage (+ 19  448) "3.22 A Purified Notion of Extensionality (for GCRs)")
;; (find-connectivespage (+ 19  453) "3.23 Some Extensionality Notions for Consequence Relations")
;; (find-connectivespage (+ 19  461) "3.24 Hybrids and the Subconnective Relation")
;; (find-connectivespage (+ 19  483) "Notes and References for §3.2")
;; (find-connectivespage (+ 19  484) "3.3 CONGRUENTIALITY")
;; (find-connectivespage (+ 19  484) "3.31 Congruential Connectives")
;; (find-connectivespage (+ 19  490) "3.32 Some Related Properties")
;; (find-connectivespage (+ 19  495) "3.33 The Three Properties Compared")
;; (find-connectivespage (+ 19  497) "3.34 Operations vs. Relations")
;; (find-connectivespage (+ 19  508) "Notes and References for §3.3")
;; (find-connectivespage (+ 19  513)   "Inversion Principle")
;; (find-connectivestext (+ 19  513)   "Inversion Principle")
;; (find-connectivespage (+ 19 1440) "Index")
;; (find-connectivestext "")



;; «hurd»  (to ".hurd")
;; http://gigapedia.com/items/107986/nonstandard-analysis---recent-developments--lecture-notes-in-mathematics---vol--983
(code-djvu       "hurd0983" "~/books/__logic/hurd__nonstandard_analysis_recent_developments_slnm0983.djvu")
(code-djvutotext "hurd0983" "~/books/__logic/hurd__nonstandard_analysis_recent_developments_slnm0983.djvu")
;; (find-hurd0983page        4  "Contents")
;; (find-hurd0983page (+ 5 120) "Laugwitz")
;; (find-hurd0983text "")

;; «hurd-loeb»  (to ".hurd-loeb")
;; http://gigapedia.com/items/107985/victoria-symposium-on-nonstandard-analysis--university-of-victoria-1972
(code-djvu       "victoria0369" "~/books/__logic/hurd_loeb__victoria_symposium_on_nonstandard_analysis_SLNM0369.djvu")
(code-djvutotext "victoria0369" "~/books/__logic/hurd_loeb__victoria_symposium_on_nonstandard_analysis_SLNM0369.djvu")
;; (find-victoria0369page        12  "Contents")
;; (find-victoria0369page (+ 17 122) "Kock/Mikkelsen" "Topos-theoretic factorization...)
;; (find-victoria0369page (+ 17 313) "Index")
;; (find-victoria0369text "")

;; http://gigapedia.com/items/194193/an-introduction-to-nonstandard-real-analysis--volume-118--pure-and-applied-mathematics-
(code-djvu       "~/books/__logic/hurdloebintro" "hurd_loeb__an_introduction_to_nonstandard_real_analysis.djvu")
(code-djvutotext "~/books/__logic/hurdloebintro" "hurd_loeb__an_introduction_to_nonstandard_real_analysis.djvu")
;; (find-~/books/__logic/hurdloebintropage         7  "Contents")
;; (find-~/books/__logic/hurdloebintropage (+ 12 225) "List of Symbols")
;; (find-~/books/__logic/hurdloebintropage (+ 12 227) "Index")
;; (find-~/books/__logic/hurdloebintrotext "")

;; «jamnik» (to ".jamnik")
;; (find-books "__logic/__logic.el" "jamnik")
(code-pdf       "jamnikmrd" "~/books/__logic/jamnik__mathematical_reasoning_with_diagrams.pdf")
(code-pdftotext "jamnikmrd" "~/books/__logic/jamnik__mathematical_reasoning_with_diagrams.pdf" 1)
(code-pdf       "jamnikdrai" "~/books/__logic/jamnik_ed__diagrammatic_representation_and_inference.pdf")
(code-pdftotext "jamnikdrai" "~/books/__logic/jamnik_ed__diagrammatic_representation_and_inference.pdf" 1)
;; (find-jamnikmrdpage)
;; (find-jamnikmrdtext "")
;; (find-jamnikmrdpage (+ 8 1) "1 Introduction")
;; (find-jamnikmrdpage (+ 8 11) "2 The History of Diagrammatic Systems")
;; (find-jamnikmrdpage (+ 7 27) "3 Diagrammatic Theorems and the Problem Domain")
;; (find-jamnikmrdpage (+ 6 49) "4 The Constructive -Rule and Schematic Proofs")
;; (find-jamnikmrdpage (+ 5 71) "5 Designing a Diagrammatic Reasoning System")
;; (find-jamnikmrdpage (+ 5 89) "6 Diagrammatic Operations")
;; (find-jamnikmrdpage (+ 5 103) "7 The Construction of Schematic Proofs")
;; (find-jamnikmrdpage (+ 4 123) "8 The Verification of Schematic Proofs")
;; (find-jamnikmrdpage (+ 3 149) "9 Diamond in Action")
;; (find-jamnikmrdpage (+ 3 163) "10 Complete Automation")
;; (find-jamnikmrdpage (+ 2 175) "Appendix A: More Examples of Diagrammatic Theorems")
;; (find-jamnikmrdpage (+ 2 181) "Appendix B: The -Rule")
;; (find-jamnikmrdpage (+ 2 185) "Glossary")
;; (find-jamnikmrdpage (+ 2 190) "References")
;; (find-jamnikmrdpage (+ 2 199) "Index")

;; (find-jamnikdraipage)
;; (find-jamnikdraipage         8  "Contents")
;; (find-jamnikdraitext         8  "Contents")
;; (find-jamnikdraipage (+ 12  84) "Index")
;; (find-jamnikdraipage (+ 0  310) "Index")
;; (find-jamnikdraitext "")



;; «kelley»  (to ".kelley")
;; http://gigapedia.com/items/100530/general-topology--graduate-texts-in-mathematics-
(code-djvu "kelley" "~/books/__logic/kelley__general_topology.djvu")
;; (find-kelleypage        10  "Contents")
;; (find-kelleypage (+ 16 250) "Elementary Set Theory")
;; (find-kelleypage (+ 16 293) "Index")

;; «kleene»  (to ".kleene")
;; http://gigapedia.com/items/124942/introduction-to-metamathematics--bibliotheca-mathematica---bibliotheca-mathematica-
(code-djvu "kleeneintrometa" "~/books/__logic/kleene__introduction_to_metamathematics.djvu")
;; (find-kleeneintrometapage      3  "Contents")
;; (find-kleeneintrometapage (+ -265 539) "Index")

;; «knuth»  (to ".knuth")
;; http://gigapedia.com/items/105202/surreal-numbers
(code-djvu "surrealnumbers" "~/books/__logic/knuth__surreal_numbers.djvu")
;; (find-surrealnumberspage      3  "Contents")
;; (find-surrealnumberspage (+ 3 6) "In the beginning")

;; «kohlenbach»  (to ".kohlenbach")
;; http://gigapedia.org/items/210283/proof-interpretations
(code-xpdf      "kohlenbach" "~/books/__logic/kohlenbach__proof_interpretations.pdf")
;; (find-kohlenbachpage        9  "Contents")
;; (find-kohlenbachpage (+ 10 50) "6. Negative Translation")

;; «kripke» (to ".kripke")
;; (find-books "__logic/__logic.el" "kripke")
(code-pdf       "kripkenan" "~/books/__logic/kripke__naming_and_necessity.pdf")
(code-pdftotext "kripkenan" "~/books/__logic/kripke__naming_and_necessity.pdf" 1)
;; (find-kripkenanpage)
;; (find-kripkenanpage        1  "Contents")
;; (find-kripkenanpage (+ 1 189) "Index")
;; (find-kripkenantext "")

;; «krivine»  (to ".krivine")
(code-djvu "kreiselkrivine"    "~/books/__logic/kreisel_krivine__elements_of_mathematical_logic__model_theory.djvu")
(code-djvu        "krivinetae" "~/books/__logic/krivine__theorie_axiomatique_des_ensembles.djvu")
(code-xpdf        "krivinete"  "~/books/__logic/krivine__theorie_des_ensembles.pdf")
(code-pdftotext   "krivinete"  "~/books/__logic/krivine__theorie_des_ensembles.pdf")
;; (find-kreiselkrivinepage      1  "Contents")
;; (find-kreiselkrivinepage (+ 1 1) "Index")
;; (find-krivinetaepage (+ -2 9) "1. Axiomes de la Theorie des Ensembles")
;; (find-krivinetaepage     118  "Table des Matieres")
;; (find-krivinetepage (+ 8   7)  "1. Axiomes de Zermelo-Fraenkel")
;; (find-krivinetepage (+ 8 265) "Index")
;; (find-krivinetepage (+ 8 271) "Table des Matieres")
;; (find-krivinetetext)

;; «kunen»  (to ".kunen")
;; http://gigapedia.com/items/209494/set-theory--studies-in-logic-and-the-foundations-of-mathematics---studies-in-logic-and-the-foundations-of-mathematics-
(code-djvu "kunen" "~/books/__logic/kunen__set_theory.djvu")
;; (find-kunenpage         6  "Contents")
;; (find-kunenpage (+ 14 311) "Index")

;; «landau»  (to ".landau")
;; (find-angg ".emacs.papers" "automath")
;; http://gigapedia.com/items/46452/foundations-of-analysis---the-arithmetic-of-whole--rational--irrational--and-complex-numbers--a-supplement-to-textbooks-on-the-differential-and-integral-calculus
(code-djvu "landaufoa" "~/books/__logic/landau__foundations_of_analysis.djvu")
;; (find-landaufoapage        12  "Contents")
;; (find-landaufoapage (+ 13 135) "Index")

;; «luxemburg-robinson»  (to ".luxemburg-robinson")
;; http://gigapedia.com/items/374065/contributions-to-non-standard-analysis--studies-in-logic-and-the-foundations-of-mathematics-69-
(code-xpdf      "luxemburgrobcontrnsa" "~/books/__logic/luxemburg_robinson__contributions_to_nonstandard_analysis.pdf")
(code-pdftotext "luxemburgrobcontrnsa" "~/books/__logic/luxemburg_robinson__contributions_to_nonstandard_analysis.pdf")
;; (find-luxemburgrobcontrnsapage         1  "Contents")
;; (find-luxemburgrobcontrnsapage (+  4   1) "Robinson")
;; (find-luxemburgrobcontrnsapage (+ -4 281) "Jensen")
;; (find-luxemburgrobcontrnsatext "")

;; «machover»  (to ".machover")
;; http://gigapedia.com/items/251013/set-theory--logic-and-their-limitations
(code-djvu "macoverstll" "~/books/__logic/machover__set_theory_logic_and_their_limitations.djvu")
;; (find-macoverstllpage         9  "Contents")
;; (find-macoverstllpage (+ 14   1) "0. Mathematical induction")
;; (find-macoverstllpage (+ 14   9) "1. Sets and classes")
;; (find-macoverstllpage (+ 14 284) "General index")

;; «machover-hirschfeld»  (to ".machover-hirschfeld")
(code-djvu      "machoverhischfeld" "~/books/__logic/machover_hirschfeld__lectures_on_non-standard_analysis.djvu")
(code-pdftotext "machoverhischfeld" "~/books/__logic/machover_hirschfeld__lectures_on_non-standard_analysis.djvu")
;; (find-machoverhischfeldpage       5  "Contents")
;; (find-machoverhischfeldpage (+ 6 17) "Index")
;; (find-machoverhischfeldtext "")

;; «marcos» (to ".marcos")
;; (find-books "__logic/__logic.el" "marcos")
;; https://sites.google.com/site/sequiturquodlibet/courses/lc-dgm
(code-pdf       "marcoslc1"  "~/books/__logic/marcos__logica_computacional__cap1.pdf")
(code-pdftotext "marcoslc1"  "~/books/__logic/marcos__logica_computacional__cap1.pdf" 1)
(code-pdf       "marcoslc2"  "~/books/__logic/marcos__logica_computacional__cap2.pdf")
(code-pdftotext "marcoslc2"  "~/books/__logic/marcos__logica_computacional__cap2.pdf" 1)
(code-pdf       "marcoslc31" "~/books/__logic/marcos__logica_computacional__cap3_v1.pdf")
(code-pdftotext "marcoslc31" "~/books/__logic/marcos__logica_computacional__cap3_v1.pdf" 1)
(code-pdf       "marcoslc32" "~/books/__logic/marcos__logica_computacional__cap3_v2.pdf")
(code-pdftotext "marcoslc32" "~/books/__logic/marcos__logica_computacional__cap3_v2.pdf" 1)
(code-pdf       "marcoslc4"  "~/books/__logic/marcos__logica_computacional__cap4.pdf")
(code-pdftotext "marcoslc4"  "~/books/__logic/marcos__logica_computacional__cap4.pdf" 1)
;; (find-marcoslc1page)
;; (find-marcoslc1page "Lógica proposicional")
;; (find-marcoslc1text "")

;; (find-marcoslc2page)
;; (find-marcoslc2page 1  "Conteúdo")
;; (find-marcoslc2page 3  "Lóogica proposicional em Isabelle")
;; (find-marcoslc2page (+ 1 189) "Index")
;; (find-marcoslc2text "")

;; (find-marcoslc31page)
;; (find-marcoslc31page 1 "Lógica de primeira ordem")
;; (find-marcoslc31text "")

;; (find-marcoslc32page)
;; (find-marcoslc32page 1 "Lógica de primeira ordem")
;; (find-marcoslc32text "")

;; (find-marcoslc4page)
;; (find-marcoslc4page 1 "Lógica Modal")
;; (find-marcoslc4text "")




;; «martin-lof»  (to ".martin-lof")
;; http://gigapedia.com/items/260202/intuitionistic-type-theory--notes-by-giovanni-sambin-of-a-series-of-lectures-given-in-padua--june-1980--studies-in-proof-theory-
(code-djvu "martinlofitt" "~/books/__logic/martin-lof__an_intuitionistic_type_theory.djvu")
;; (find-martinlofittpage      4  "Contents")
;; (find-martinlofittpage (+ 9 1) "Introductory remarks")

(code-pdf       "martinlofdurante" "~/books/__logic/martin-lof_durante__on_the_meanings_of_the_logical_constants.pdf")
(code-pdftotext "martinlofdurante" "~/books/__logic/martin-lof_durante__on_the_meanings_of_the_logical_constants.pdf" 1)
;; (find-martinlofdurantepage)
;; (find-martinlofdurantepage        1  "Contents")
;; (find-martinlofdurantepage (+ 1 189) "Index")
;; (find-martinlofdurantetext "")


;; «mints»  (to ".mints")
;; http://gigapedia.com/items/54694/a-short-introduction-to-intuitionistic-logic--university-series-in-mathematics---university-series-in-mathematics-
(code-xpdf      "mintssiil" "~/books/__logic/mints__a_short_introduction_to_intuitionistic_logic.pdf")
(code-pdftotext "mintssiil" "~/books/__logic/mints__a_short_introduction_to_intuitionistic_logic.pdf")
;; (find-mintssiilpage         6  "Contents")
;; (find-mintssiilpage (+  8   1) "Introduction")
;; (find-mintssiilpage (+ -2 129) "Index")
;; (find-mintssiiltext)

;; «mortari»  (to ".mortari")
(code-djvu       "mortari" "~/books/__logic/mortari__introducao_a_logica.djvu")
(code-djvutotext "mortari" "~/books/__logic/mortari__introducao_a_logica.djvu" 1)
;; (find-mortaripage)
;; (find-mortaripage        1  "Contents")
;; (find-mortaripage (+ 1 189) "Index")
;; (find-mortaritext "")


;; «mortensen» (to ".mortensen")
(code-pdf       "mortensen" "~/books/__logic/mortensen__inconsistent_mathematics.pdf")
(code-pdftotext "mortensen" "~/books/__logic/mortensen__inconsistent_mathematics.pdf" 10)
;; (find-mortensenpage)
;; (find-mortensenpage         7  "Contents")
;; (find-mortensenpage (+ 10 152) "Index")
;; (find-mortensentext "")

;; (find-mortensenpage (+ 10 1) "ONE     MOTIVATIONS")
;; (find-mortensentext (+ 10 1) "ONE     MOTIVATIONS")
;; (find-mortensenpage (+ 10 1) "        1.   Paraconsistency")
;; (find-mortensentext (+ 10 1) "        1.   Paraconsistency")
;; (find-mortensenpage (+ 10 5) "        2.   Summary")
;; (find-mortensentext (+ 10 5) "        2.   Summary")
;; (find-mortensenpage (+ 10 7) "        3.   Philosophical Implications")
;; (find-mortensentext (+ 10 7) "        3.   Philosophical Implications")
;; (find-mortensenpage (+ 10 15) "TWO     ARITHMETIC")
;; (find-mortensentext (+ 10 15) "TWO     ARITHMETIC")
;; (find-mortensenpage (+ 10 15) "        1.   Relevant Arithmetic")
;; (find-mortensentext (+ 10 15) "        1.   Relevant Arithmetic")
;; (find-mortensenpage (+ 10 20) "        2.   Nonclassical Logics and their Theories")
;; (find-mortensentext (+ 10 20) "        2.   Nonclassical Logics and their Theories")
;; (find-mortensenpage (+ 10 27) "        3.   Models for Number Systems with Arithmetical Operations")
;; (find-mortensentext (+ 10 27) "        3.   Models for Number Systems with Arithmetical Operations")
;; (find-mortensenpage (+ 10 31) "        4.   Summary of Further Results in Arithmetic")
;; (find-mortensentext (+ 10 31) "        4.   Summary of Further Results in Arithmetic")
;; (find-mortensenpage (+ 10 33) "THREE   MODULO INFINITY")
;; (find-mortensentext (+ 10 33) "THREE   MODULO INFINITY")
;; (find-mortensenpage (+ 10 33) "        1.   The Classical Denumerable Nonstandard Model of Natural Number Arithmetic")
;; (find-mortensentext (+ 10 33) "        1.   The Classical Denumerable Nonstandard Model of Natural Number Arithmetic")
;; (find-mortensenpage (+ 10 35) "        2.   Inconsistency")
;; (find-mortensentext (+ 10 35) "        2.   Inconsistency")
;; (find-mortensenpage (+ 10 39) "FOUR    ORDER")
;; (find-mortensentext (+ 10 39) "FOUR    ORDER")
;; (find-mortensenpage (+ 10 39) "        1.   Order and Equality without Function Symbols")
;; (find-mortensentext (+ 10 39) "        1.   Order and Equality without Function Symbols")
;; (find-mortensenpage (+ 10 40) "        2.   Order and Equality with Function Symbols")
;; (find-mortensentext (+ 10 40) "        2.   Order and Equality with Function Symbols")
;; (find-mortensenpage (+ 10 43) "FIVE    CALCULUS")
;; (find-mortensentext (+ 10 43) "FIVE    CALCULUS")
;; (find-mortensenpage (+ 10 43) "        1.   Introduction")
;; (find-mortensentext (+ 10 43) "        1.   Introduction")
;; (find-mortensenpage (+ 10 44) "        2.   A Nilpotent Ring of Hyperreal Numbers")
;; (find-mortensentext (+ 10 44) "        2.   A Nilpotent Ring of Hyperreal Numbers")
;; (find-mortensenpage (+ 10 47) "        3.   An Incomplete Theory")
;; (find-mortensentext (+ 10 47) "        3.   An Incomplete Theory")
;; (find-mortensenpage (+ 10 49) "        4.   Incomplete Differential Calculus")
;; (find-mortensentext (+ 10 49) "        4.   Incomplete Differential Calculus")
;; (find-mortensenpage (+ 10 55) "        5. Inconsistent Differential Calculus")
;; (find-mortensentext (+ 10 55) "        5. Inconsistent Differential Calculus")
;; (find-mortensenpage (+ 10 56) "        6. Integration")
;; (find-mortensentext (+ 10 56) "        6. Integration")
;; (find-mortensenpage (+ 10 58) "        7.   Conclusion")
;; (find-mortensentext (+ 10 58) "        7.   Conclusion")
;; (find-mortensenpage (+ 10 59) "SIX      INCONSISTENT CONTINUOUS FUNCTIONS")
;; (find-mortensentext (+ 10 59) "SIX      INCONSISTENT CONTINUOUS FUNCTIONS")
;; (find-mortensenpage (+ 10 59) "         l.   Introduction")
;; (find-mortensentext (+ 10 59) "         l.   Introduction")
;; (find-mortensenpage (+ 10 60) "         2. Functionality")
;; (find-mortensentext (+ 10 60) "         2. Functionality")
;; (find-mortensenpage (+ 10 63) "         3. Logic")
;; (find-mortensentext (+ 10 63) "         3. Logic")
;; (find-mortensenpage (+ 10 67) "SEVEN    THE DELTA FUNCTION")
;; (find-mortensentext (+ 10 67) "SEVEN    THE DELTA FUNCTION")
;; (find-mortensenpage (+ 10 67) "         l.   Introduction")
;; (find-mortensentext (+ 10 67) "         l.   Introduction")
;; (find-mortensenpage (+ 10 68) "         2. Functionality")
;; (find-mortensentext (+ 10 68) "         2. Functionality")
;; (find-mortensenpage (+ 10 73) "EIGHT    INCONSISTENT SYSTEMS OF LINEAR EQUATIONS")
;; (find-mortensentext (+ 10 73) "EIGHT    INCONSISTENT SYSTEMS OF LINEAR EQUATIONS")
;; (find-mortensenpage (+ 10 73) "         l.   Introduction")
;; (find-mortensentext (+ 10 73) "         l.   Introduction")
;; (find-mortensenpage (+ 10 73) "         2. The Inconsistent Case")
;; (find-mortensentext (+ 10 73) "         2. The Inconsistent Case")
;; (find-mortensenpage (+ 10 77) "         3. Control Theory")
;; (find-mortensentext (+ 10 77) "         3. Control Theory")
;; (find-mortensenpage (+ 10 80) "         4.   Applications, Problems and Special Cases")
;; (find-mortensentext (+ 10 80) "         4.   Applications, Problems and Special Cases")
;; (find-mortensenpage (+ 10 83) "NINE     PROJECTIVE SPACES")
;; (find-mortensentext (+ 10 83) "NINE     PROJECTIVE SPACES")
;; (find-mortensenpage (+ 10 83) "         l.   Introduction")
;; (find-mortensentext (+ 10 83) "         l.   Introduction")
;; (find-mortensenpage (+ 10 84) "         2. Vector Spaces")
;; (find-mortensentext (+ 10 84) "         2. Vector Spaces")
;; (find-mortensenpage (+ 10 86) "         3.   Projective Geometry")
;; (find-mortensentext (+ 10 86) "         3.   Projective Geometry")
;; (find-mortensenpage (+ 10 88) "         4.   Projective Geometry Modulo Infinity")
;; (find-mortensentext (+ 10 88) "         4.   Projective Geometry Modulo Infinity")
;; (find-mortensenpage (+ 10 93) "TEN      TOPOLOGY")
;; (find-mortensentext (+ 10 93) "TEN      TOPOLOGY")
;; (find-mortensenpage (+ 10 101) "ELEVEN   CATEGORY THEORY")
;; (find-mortensentext (+ 10 101) "ELEVEN   CATEGORY THEORY")
;; (find-mortensenpage (+ 10 101) "         l.   Introduction")
;; (find-mortensentext (+ 10 101) "         l.   Introduction")
;; (find-mortensenpage (+ 10 103) "         2. Closed Set Logic")
;; (find-mortensentext (+ 10 103) "         2. Closed Set Logic")
;; (find-mortensenpage (+ 10 104) "         3.   Propositional Logic in a Category")
;; (find-mortensentext (+ 10 104) "         3.   Propositional Logic in a Category")
;; (find-mortensenpage (+ 10 109) "         4.   Implication")
;; (find-mortensentext (+ 10 109) "         4.   Implication")
;; (find-mortensenpage (+ 10 112) "         5.   Quantification Theory")
;; (find-mortensentext (+ 10 112) "         5.   Quantification Theory")
;; (find-mortensenpage (+ 10 114) "         6.   Conclusion")
;; (find-mortensentext (+ 10 114) "         6.   Conclusion")
;; (find-mortensenpage (+ 10 115) "TWELVE     CLOSED SET SHEAVES AND THEIR CATEGORIES")
;; (find-mortensentext (+ 10 115) "TWELVE     CLOSED SET SHEAVES AND THEIR CATEGORIES")
;; (find-mortensenpage (+ 10 115) "           1.   Introduction")
;; (find-mortensentext (+ 10 115) "           1.   Introduction")
;; (find-mortensenpage (+ 10 116) "           2.   Pretopologies and Topologies for Categories")
;; (find-mortensentext (+ 10 116) "           2.   Pretopologies and Topologies for Categories")
;; (find-mortensenpage (+ 10 120) "           3.   Subobject Classifiers")
;; (find-mortensentext (+ 10 120) "           3.   Subobject Classifiers")
;; (find-mortensenpage (+ 10 123) "           4.   Closed Set Sheaves")
;; (find-mortensentext (+ 10 123) "           4.   Closed Set Sheaves")
;; (find-mortensenpage (+ 10 125) "THIRTEEN   DUALITY")
;; (find-mortensentext (+ 10 125) "THIRTEEN   DUALITY")
;; (find-mortensenpage (+ 10 129) "FOURTEEN   FOUNDATIONS: PROVABILITY, TRUTH AND SETS")
;; (find-mortensentext (+ 10 129) "FOURTEEN   FOUNDATIONS: PROVABILITY, TRUTH AND SETS")
;; (find-mortensenpage (+ 10 129) "           1.   Introduction")
;; (find-mortensentext (+ 10 129) "           1.   Introduction")
;; (find-mortensenpage (+ 10 130) "           2.   Provability")
;; (find-mortensentext (+ 10 130) "           2.   Provability")
;; (find-mortensenpage (+ 10 130) "                2.1 Consistent Preliminaries")
;; (find-mortensentext (+ 10 130) "                2.1 Consistent Preliminaries")
;; (find-mortensenpage (+ 10 132) "                2.2 The Inconsistent Case")
;; (find-mortensentext (+ 10 132) "                2.2 The Inconsistent Case")
;; (find-mortensenpage (+ 10 135) "           3.   Truth")
;; (find-mortensentext (+ 10 135) "           3.   Truth")
;; (find-mortensenpage (+ 10 135) "                3.1 The Fixed Point Method")
;; (find-mortensentext (+ 10 135) "                3.1 The Fixed Point Method")
;; (find-mortensenpage (+ 10 137) "                3.2 The Fixed Point Method Applied to Truth Theory")
;; (find-mortensentext (+ 10 137) "                3.2 The Fixed Point Method Applied to Truth Theory")
;; (find-mortensenpage (+ 10 139) "                3.3 The Proof that Fixed Points Model the T-scheme")
;; (find-mortensentext (+ 10 139) "                3.3 The Proof that Fixed Points Model the T-scheme")
;; (find-mortensenpage (+ 10 141) "                3.4 The Proof that there are Fixed Points")
;; (find-mortensentext (+ 10 141) "                3.4 The Proof that there are Fixed Points")
;; (find-mortensenpage (+ 10 141) "           4.   The Fixed Point Method Applied to Set Theory")
;; (find-mortensentext (+ 10 141) "           4.   The Fixed Point Method Applied to Set Theory")
;; (find-mortensenpage (+ 10 146) "           5.   Further Applications")
;; (find-mortensentext (+ 10 146) "           5.   Further Applications")
;; (find-mortensenpage (+ 10 147) "BIBLIOGRAPHY")
;; (find-mortensentext (+ 10 147) "BIBLIOGRAPHY")



;; «nederpelt»  (to ".nederpelt")
;; «automath»  (to ".automath")
;; (find-angg ".emacs.papers" "automath")
;; (to "typetheory")
;; (find-LATEX "catsem.bib" "bib-Automath")
;; http://gigapedia.org/items/194247/selected-papers-on-automath--studies-in-logic-and-the-foundations-of-mathematics-
(code-xpdf "automath" "~/books/__logic/nederpelt__selected_papers_on_automath.pdf")
;; (find-automathpage         12  "Contents")
;; (find-automathpage (+ 21 1005) "Index of subjects")

;; «nolt-rohatyn» (to ".nolt-rohatyn")
;; (find-books "__logic/__logic.el" "nolt-rohatyn")
(code-djvu       "noltro" "~/books/__logic/nolt_rohatyn__logica.djvu")
(code-djvutotext "noltro" "~/books/__logic/nolt_rohatyn__logica.djvu" 1)
;; (find-noltropage)
;; (find-noltropage        1  "Contents")
;; (find-noltropage (+ 1 189) "Index")
;; (find-noltrotext "")

;; «nordstrom»  (to ".nordstrom")
;; http://gigapedia.com/items/7759/programming-in-martin-lof--039-s-type-theory--an-introduction--international-series-of-monographs-on-computer-science-
(code-xpdf "proginmltt" "~/books/__logic/nordstrom__programming_in_martin_lofs_type_theory.pdf")
;; (find-proginmlttpage         5  "Contents")
;; (find-proginmlttpage (+ 10   1) "Introduction")
;; (find-proginmlttpage (+ 10 197) "Constants and their arities")
;; (find-proginmlttpage (+ 10 199) "Operational semantics")

;; «pohlers»  (to ".pohlers")
;; http://gigapedia.com/items/102823/proof-theory--an-introduction--lecture-notes-in-mathematics-
;; http://gigapedia.com/items/176028/proof-theory--the-first-step-into-impredicativity--universitext-
(code-xpdf "pohlersintro"  "~/books/__logic/pohlers__proof_theory_an_introduction.pdf")
(code-xpdf "pohlersimpled" "~/books/__logic/pohlers__proof_theory_the_first_step_into_impredicativity.pdf")
;; (find-pohlersintropage        5  "Contents")
;; (find-pohlersintropage (+ 6 208) "Subject index")
;; (find-pohlersimpledpage        9  "Contents")
;; (find-pohlersimpledpage (+ 6 363) "Index")

;; «prawitz»  (to ".prawitz")
(code-pdf       "prawitz" "~/books/__logic/prawitz__natural_deduction.pdf")
(code-pdftotext "prawitz" "~/books/__logic/prawitz__natural_deduction.pdf" -4)
;; (find-books "__logic/__logic.el" "prawitz")
;; (find-angg ".emacs.papers" "wadler-pat")
;; (find-prawitzpage         6  "Contents")
;; (find-prawitzpage (+ -4  19) "The corresponding natural deduction is given below")
;; (find-prawitzpage (+ -4  13) "I. Natural Deduction of Gentzen Type")
;; (find-prawitzpage (+ -4  32) "II. The Inversion Principle")
;; (find-prawitzpage (+ -4  39) "III. Normal Deductions in Classical Logic")
;; (find-prawitzpage (+ -4  49) "IV. Normal Deductions in Intuitionistic Logic")
;; (find-prawitzpage (+ -4  63) "V. Second Order Logic")
;; (find-prawitzpage (+ -4  49) "Theorem on normal deductions")
;; (find-prawitzpage (+ -4  67) "Definability of and, or, ex and bot")
;; (find-prawitzpage (+ -4  72) "=")
;; (find-prawitzpage (+ -4  90) "Connections between the calculus of sequents and the systems of natural deduction")
;; (find-prawitzpage (+ -4  94) "The originis of natural deduction")
;; (find-prawitzpage (+ -4 104) "Copi")
;; (find-prawitzpage (+ -4 110) "Index")

;; (find-prawitzpage)
;; (find-prawitzpage        1  "Contents")
;; (find-prawitzpage (+ 1 189) "Index")
;; (find-prawitztext "")


;; «reynolds» (to ".reynolds")
;; (find-books "__logic/__logic.el" "reynolds")
;; https://doi.org/10.1007/3-540-13346-1_7
;; http://h2.jaguarpaw.co.uk/posts/polymorphism-is-not-set-theoretic/
(code-pdf       "pinst" "~/books/__logic/reynolds__polymorphism_is_not_set-theoretic.pdf")
(code-pdftotext "pinst" "~/books/__logic/reynolds__polymorphism_is_not_set-theoretic.pdf" -144)
;; (find-pinstpage)
;; (find-pinstpage (+ -144 145) "Introduction")
;; (find-pinsttext "")



;; «robinson»  (to ".robinson")
;; (find-LATEX "filters.bib" "robinson")
;; http://gigapedia.com/items/255512/introduction-to-model-theory-and-to-the-metamathematics-of-algebra--studies-in-logic-and-the-foundations-of-mathematics-
;; http://gigapedia.com/items/255510/non-standard-analysis--studies-in-logic-and-the-foundations-of-mathematics-
(code-xpdf "robinsonmtma" "~/books/__logic/robinson__introduction_to_model_theory_and_to_the_metamathematics_of_algebra.pdf")
(code-xpdf "robinsonnsa"  "~/books/__logic/robinson__non-standard_analysis.pdf")
;; (find-robinsonmtmapage (+ 4   1) "Chapter 1")
;; (find-robinsonmtmapage (+ 4 244) "9.4. Non-standard analysis")
;; (find-robinsonnsapage (+ 6   1) "Chapter 1")
;; (find-robinsonnsapage (+ 6 292) "Subject Index")

;; «rose-shepherdson»  (to ".rose-shepherdson")
;; http://gigle.ws/logic-colloquium--039-73-proceedings-of-the-logic-colloquium-bristol-july-1973_.1086791.html
(code-xpdf      "logiccolloquim73" "~/books/__logic/rose_shepherdson__logic_colloquim_73.pdf")
(code-pdftotext "logiccolloquim73" "~/books/__logic/rose_shepherdson__logic_colloquim_73.pdf")
;; (find-logiccolloquim73page      1  "Contents")
;; (find-logiccolloquim73page (+ 1 5) "Bernays")
;; (find-logiccolloquim73page (+ 5 5) "Dummett")
;; (find-logiccolloquim73page (+ 3 43) "Robinson")
;; (find-logiccolloquim73page (+ 2 75) "Martin-Löf")
;; (find-logiccolloquim73page (+ 2 121) "MacLane")
;; (find-logiccolloquim73page (+ 2 137) "Lawvere")
;; (find-logiccolloquim73page (+ 4 157) "Milner")
;; (find-logiccolloquim73page (+ 3 175) "Elgot")
;; (find-logiccolloquim73page (+ 3 231) "Engeler")
;; (find-logiccolloquim73page (+ 3 432) "Seldin")
;; (find-logiccolloquim73text "")

;; «russell» (to ".russell")
(code-pdf       "russellml" "~/books/__logic/russell__mysticism_and_logic.pdf")
(code-pdftotext "russellml" "~/books/__logic/russell__mysticism_and_logic.pdf" 1)
;; (find-russellmlpage)
;; (find-russellmlpage        1  "Contents")
;; (find-russellmlpage (+ 1 189) "Index")
;; (find-russellmltext "")

;; «sambin-smith»  (to ".sambin-smith")
;; «ctt»  (to ".ctt")
;; http://gigapedia.com/items/120092/twenty-five-years-of-constructive-type-theory--proceedings-of-a-congress-held-in-venice--october-1995--oxford-logic-guides-
(code-xpdf "25yctt" "~/books/__logic/sambin_smith__25_years_of_constructive_type_theory.pdf")
;; (find-25ycttpage        5  "Preface")
;; (find-25ycttpage        8  "Contents")
;; (find-25ycttpage (+ 8  83) "Hoffman" "Streicher" "The grupoid interpretation of type theory")
;; (find-25ycttpage (+ 8 127) "An intuitionistic theory of types" "Per Martin-Löf")
;; (find-25ycttpage (+ 8 133) "An intuitionistic theory of types" "Girard's paradox")
;; (find-25ycttpage (+ 8 191) "On universes in type theory" "Erik Palmgren")
;; (find-25ycttpage (+ 8 221) "Building up a toolbox for Martin-Löf's Type Theory: subset theory" "Sambin" "Valentini")

;; «saracino-weispfenning»  (to ".saracino-weispfenning")
;; http://gigapedia.com/items/72741/model-theory-and-algebra--a-memorial-tribute-to-abraham-robinson--lecture-notes-in-mathematics---498-
(code-djvu "slnm498" "~/books/__logic/saracino_weispfenning_eds__model_theory_and_algebra_slnm0498.djvu")
;; (find-slnm498page       6  "Contents")
;; (find-slnm498page (+ 7 14) "Algorithms in Algebra")

;; «scheele» (to ".scheele")
;; (find-books "__logic/__logic.el" "scheele")
(code-pdf       "sheelealc" "~/books/__logic/scheele__model_and_proof_theory_of_constructive_ALC.pdf")
(code-pdftotext "sheelealc" "~/books/__logic/scheele__model_and_proof_theory_of_constructive_ALC.pdf" 1)
;; (find-sheelealcpage)
;; (find-sheelealcpage       10  "Abstract")
;; (find-sheelealcpage       16  "Contents")
;; (find-sheelealcpage (+ 1 189) "Index")
;; (find-sheelealctext "")

;; «smullyan» (to ".smullyan")
;; (find-books "__logic/__logic.el" "smullyan")
(code-pdf       "smullyanfol" "~/books/__logic/smullyan__first-order_logic.pdf")
(code-pdftotext "smullyanfol" "~/books/__logic/smullyan__first-order_logic.pdf" 14)
;; (find-smullyanfolpage)
;; (find-smullyanfolpage        13  "Contents")
;; (find-smullyanfolpage (+ 14   3) "Index")
;; (find-smullyanfolpage (+ 14  15) "II. Analytic Tableaux")
;; (find-smullyanfolpage (+ 14 157) "Index")
;; (find-smullyanfoltext "")

;; «spencer-brown» (to ".spencer-brown")
;; (find-books "__logic/__logic.el" "spencer-brown")
(code-pdf       "lawsofform" "~/books/__logic/spencer-brown__laws_of_form.pdf")
(code-pdftotext "lawsofform" "~/books/__logic/spencer-brown__laws_of_form.pdf" 26)
;; (find-lawsofformpage)
;; (find-lawsofformpage         3  "Contents")
;; (find-lawsofformpage (+ 26 138) "Index of forms")
;; (find-lawsofformtext "")

;; «stenlund»  (to ".stenlund")
;; http://gigapedia.com/items/39544/combinators--lambda-terms-and-proof-theory--synthese-library-
(code-djvu "stenlund" "~/books/__logic/stenlund__combinators_lambda_terms_and_proof_theory.djvu")
;; (find-stenlundpage        7  "Contents")
;; (find-stenlundpage (+ 0  71) "combinatorial completeness" "deductive completeness")
;; (find-stenlundpage (+ 0  92) "combinatorial definability")
;; (find-stenlundpage (+ 0 182) "Index")

;; «stroyan»  (to ".stroyan")
;; http://gigapedia.com/items/108825/mathematical-background--foundations-of-infinitesimal-calculus--2nd-edition
(code-xpdf      "stroyanbg" "~/books/__logic/stroyan__mathematical_background__foundations_of_infinitesimal_calculus.pdf")
(code-pdftotext "stroyanbg" "~/books/__logic/stroyan__mathematical_background__foundations_of_infinitesimal_calculus.pdf")
;; (find-stroyanbgpage      1  "Contents")
;; (find-stroyanbgpage (+ 1 1) "Index")
;; (find-stroyanbgtext "")

;; «stroyan-luxemburg»  (to ".stroyan-luxemburg")
;; http://gigapedia.com/items/362432/introduction-to-the-theory-of-infinitesimals--pure-and-applied-mathematics--a-series-of-monographs-and-textbooks--72-
(code-xpdf      "stroyanluxemburg" "~/books/__logic/stroyan_luxemburg__introduction_to_the_theory_of_infinitesimals.pdf")
(code-pdftotext "stroyanluxemburg" "~/books/__logic/stroyan_luxemburg__introduction_to_the_theory_of_infinitesimals.pdf")
;; (find-stroyanluxemburgpage         8  "Contents")
;; (find-stroyanluxemburgpage (+ 17 323) "Index")
;; (find-stroyanluxemburgtext "")

;; «tarski»  (to ".tarski")
;; http://gigapedia.com/items/113463/introduction-to-logic-and-to-the-methodology-of-the-deductive-sciences--oxford-logic-guides-
(code-djvu "tarskilameds" "~/books/__logic/tarski__introduction_to_logic_and_to_the_methodology_of_the_deductive_sciences.djvu")
;; (find-tarskilamedspage         6  "Contents")
;; (find-tarskilamedspage (+ 25   3) "Index")
;; (find-tarskilamedspage (+ 25 213) "Index")

;; «tarskiaot» (to ".tarskiaot")
;; https://www.dimap.ufrn.br/~jmarcos/papers/AoT-McKinsey_Tarski.pdf
;; McKinsey/Tarski: The Algebra of Topology (1944)
;; http://www.jstor.org/stable/1969080
;; (find-fline "$S/https/www.dimap.ufrn.br/~jmarcos/papers/")
(code-xpdf     "tarskiaot" "$S/https/www.dimap.ufrn.br/~jmarcos/papers/AoT-McKinsey_Tarski.pdf")
(code-pdf-text "tarskiaot" "$S/https/www.dimap.ufrn.br/~jmarcos/papers/AoT-McKinsey_Tarski.pdf" -139)
;; (find-tarskiaotpage)
;; (find-tarskiaotpage (+ -139 141))
;; (find-tarskiaottext)

;; «tarskisclh» (to ".tarskisclh")
;; McKinsey/Tarski: Some Theorems About the Sentential Calculi of Lewis and Heyting (1948)
;; http://www.jstor.org/stable/2268135 .
;; (find-fline "~/books/__logic/" "mckinsey-tarski_1948.pdf")
;; (find-fline "~/books/__logic/")
(code-xpdf     "tarskisclh" "~/books/__logic/mckinsey-tarski_1948.pdf")
(code-pdf-text "tarskisclh" "~/books/__logic/mckinsey-tarski_1948.pdf" 1)
;; (find-tarskisclhpage)
;; (find-tarskisclhtext)
;; (find-tarskisclhpage (+ 1 1) "1. The Lewis system and closure algebra")
;; (find-tarskisclhtext (+ 1 1) "1. The Lewis system and closure algebra")




;; «van_dalen» (to ".van_dalen")
;; (find-books "__logic/__logic.el" "van_dalen")
(code-xpdf      "vdls" "~/books/__logic/van_dalen__logic_and_structure.pdf")
(code-pdftotext "vdls" "~/books/__logic/van_dalen__logic_and_structure.pdf" 8)
;; (find-vdlspage)
;; (find-vdlspage        8  "Contents")
;; (find-vdlspage (+ 1 189) "Index")
;; (find-vdlstext "")
;; (find-vdlspage (+ 8 60) "2.3 The Language of a Similarity Type")
;; (find-vdlspage (+ 8 68) "2.3 The Language of a Similarity Type")
;; (find-vdlstext (+ 8 68) "2.3 The Language of a Similarity Type")


;; «vandenberg-neves»  (to ".vandenberg-neves")
;; «nsa»  (to ".nsa")
;; http://gigapedia.org/items/89038/the-strength-of-nonstandard-analysis
(code-djvu "strengthofnsa" "~/books/__logic/van_den_berg_neves__the_strength_of_NSA.djvu")
;; (find-strengthofnsapage        12  "Contents")
;; (find-strengthofnsapage (+ 18  27) "Nelson")
;; (find-strengthofnsapage (+ 18  33) "Péraire")
;; (find-strengthofnsapage (+ 18 369) "24. Calculus with infinitesimals" "Keith D. Stroyan")







;; «games»  (to ".games")
;; http://gigapedia.com/items/255472/games--unifying-logic--language--and-philosophy--logic--epistemology--and-the-unity-of-science-
(code-xpdf "gullap" "~/books/__logic/majer_pietarinen_eds__games_unifying_logic_language_and_philosophy.pdf")
;; (find-gullappage         6  "Contents")
;; (find-gullappage (+ 13 373) "Subject Index")

;; «tableaux»  (to ".tableaux")
;; http://gigapedia.com/items/68358/handbook-of-tableau-methods
;; http://www.dcs.kcl.ac.uk/research/groups/gllc/publications/handbooks.html
(code-xpdf "tableaumethods" "~/books/__logic/dagostino_gabbay_eds__handbook_of_tableau_methods.pdf")
;; (find-tableaumethodspage        4  "Contents")
;; (find-tableaumethodspage (+ 7   1) "Melvin Fitting - Introduction")
;; (find-tableaumethodspage (+ 7 125) "First-order tableau methods")
;; (find-tableaumethodspage (+ 7 255) "Tableaux for Intuitionistic Logics")
;; (find-tableaumethodspage (+ 7 657) "Index")

;; «typetheory»  (to ".typetheory")
;; (find-LATEX "catsem.bib" "bib-Kamareddine")
;; http://gigapedia.com/items/80801/a-modern-perspective-on-type-theory--from-its-origins-until-today--applied-logic-series-
(code-xpdf      "mpott" "~/books/__logic/kamareddine_laan_nederpelt__a_modern_perspective_on_type_theory.pdf")
(code-pdftotext "mpott" "~/books/__logic/kamareddine_laan_nederpelt__a_modern_perspective_on_type_theory.pdf")
;; (find-mpottpage         5  "Contents")
;; (find-mpottpage (+ 10 349) "Subject index")
;; (find-mpottpage (+ 12 231) "8.   Pure Type Systems with  definitions")
;; (find-mpotttext    "Chapter 8\n\nPure Type Systems with\ndefinitions")
;; (find-mpottpage (+ 10 243) "9    The Barendregt cube with  parameters")
;; (find-mpotttext    "Chapter 9\n\nThe Barendregt cube with\nparameters")
;; (find-mpottpage (+ 10 255) "10    Pure Type Systems with  parameters and definitions")
;; (find-mpotttext    "Chapter 10\n\nPure Type Systems with\nparameters and definitions")
;; (find-mpotttext )





;; http://gigapedia.com/items/120386/domains-and-lambda-calculi--cambridge-tracts-in-theoretical-computer-science-
(code-xpdf      "amadiocurien" "~/books/__logic/amadio_curien__domains_and_lambda_calculi.pdf")
(code-pdftotext "amadiocurien" "~/books/__logic/amadio_curien__domains_and_lambda_calculi.pdf" 2)
;; (find-amadiocurienpage       3  "Contents")
;; (find-amadiocurienpage (+ 2 13) "Chapter 1")
;; (find-amadiocurientext "")
;; (find-amadiocurienpage (+ 2 13) "1 Continuity and Computability")
;; (find-amadiocurientext (+ 2 13) "1 Continuity and Computability")
;; (find-amadiocurienpage (+ 2 35) "2 Syntactic Theory of the -calculus")
;; (find-amadiocurientext (+ 2 35) "2 Syntactic Theory of the -calculus")
;; (find-amadiocurienpage (+ 2 57) "3 D1 Models and Intersection Types")
;; (find-amadiocurientext (+ 2 57) "3 D1 Models and Intersection Types")
;; (find-amadiocurienpage (+ 2 87) "4 Interpretation of -Calculi in CCC's")
;; (find-amadiocurientext (+ 2 87) "4 Interpretation of -Calculi in CCC's")
;; (find-amadiocurienpage (+ 2 123) "5 CCC's of Algebraic Dcpo's")
;; (find-amadiocurientext (+ 2 123) "5 CCC's of Algebraic Dcpo's")
;; (find-amadiocurienpage (+ 2 145) "6 The Language PCF")
;; (find-amadiocurientext (+ 2 145) "6 The Language PCF")
;; (find-amadiocurienpage (+ 2 167) "7 Domain Equations")
;; (find-amadiocurientext (+ 2 167) "7 Domain Equations")
;; (find-amadiocurienpage (+ 2 191) "8 Values and Computations")
;; (find-amadiocurientext (+ 2 191) "8 Values and Computations")
;; (find-amadiocurienpage (+ 2 225) "9 Powerdomains")
;; (find-amadiocurientext (+ 2 225) "9 Powerdomains")
;; (find-amadiocurienpage (+ 2 241) "10 Stone Duality")
;; (find-amadiocurientext (+ 2 241) "10 Stone Duality")
;; (find-amadiocurienpage (+ 2 267) "11 Dependent and Second Order Types")
;; (find-amadiocurientext (+ 2 267) "11 Dependent and Second Order Types")
;; (find-amadiocurienpage (+ 2 299) "12 Stability")
;; (find-amadiocurientext (+ 2 299) "12 Stability")
;; (find-amadiocurienpage (+ 2 335) "13 Towards Linear Logic")
;; (find-amadiocurientext (+ 2 335) "13 Towards Linear Logic")
;; (find-amadiocurienpage (+ 2 379) "14 Sequentiality")
;; (find-amadiocurientext (+ 2 379) "14 Sequentiality")
;; (find-amadiocurienpage (+ 2 429) "15 Domains and Realizability")
;; (find-amadiocurientext (+ 2 429) "15 Domains and Realizability")
;; (find-amadiocurienpage (+ 2 465) "16 Functions and Processes")
;; (find-amadiocurientext (+ 2 465) "16 Functions and Processes")
;; (find-amadiocurienpage (+ 2 495) "A Memento of Recursion Theory")
;; (find-amadiocurientext (+ 2 495) "A Memento of Recursion Theory")
;; (find-amadiocurienpage (+ 2 501) "B Memento of Category")
;; (find-amadiocurientext (+ 2 501) "B Memento of Category")






(code-djvu "howtowritemath" "~/books/__logic/steenrod_halmos_schiffer_dieudonne__how_to_write_mathematics.djvu")
;; (find-howtowritemathpage (+ 7  1) "Steenrod")
;; (find-howtowritemathpage (+ 7 19) "Halmos")
;; (find-howtowritemathpage (+ 7 49) "Schiffer")
;; (find-howtowritemathpage (+ 7 63) "Dieudonne")
(code-djvu       "naivesettheory" "~/books/__logic/halmos__naive_set_theory.djvu")
(code-djvutotext "naivesettheory" "~/books/__logic/halmos__naive_set_theory.djvu")
;; (find-naivesettheorypage         9  "Contents")
;; (find-naivesettheorypage (+ 10 102) "Index")
;; (find-naivesettheorytext "")
(code-djvu       "logicasalgebra" "~/books/__logic/halmos_givant__logic_as_algebra.djvu")
(code-djvutotext "logicasalgebra" "~/books/__logic/halmos_givant__logic_as_algebra.djvu")
;; (find-logicasalgebrapage        5  "Contents")
;; (find-logicasalgebrapage (+ 8 135) "Index")
;; (find-logicasalgebratext "")




;; http://gigapedia.com/items/360847/journal-of-automated-reasoning--1985-2008-


;; http://www.polimetrica.com/main/list.php
;; ~/books/__logic/slater__the_demathematisation_of_logic__openaccess.pdf

;; http://gigapedia.org/items/44097/types-and-programming-languages
;; ~/books/__logic/pierce__types_and_programming_languages.chm
;; (find-unpack-chm-links "~/books/__logic/pierce__types_and_programming_languages.chm" "~/usrc/piercetapl/" "piercetapl")
;; Broken?

(code-xpdf "vellerman" "~/books/__logic/vellerman__how_to_prove_it.pdf")
;; (find-vellermanpage         9  "Contents")
;; (find-vellermanpage (+ 14 381) "Index")



;; http://gigapedia.com/items/99143/residuated-lattices--an-algebraic-glimpse-at-substructural-logics--volume-151--studies-in-logic-and-the-foundations-of-mathematics---studies-in-logic-and-the-foundations-of-mathematics-
;; http://gigapedia.com/items/101018/substructural-logics--a-primer--trends-in-logic-
;; http://gigapedia.com/items/353519/substructural-logics--studies-in-logic-and-computation-
;; http://gigapedia.com/items/113448/quantification-in-nonclassical-logic--studies-in-logic-and-the-foundations-of-mathematics-
;; http://gigapedia.com/items/99488/analysis-and-synthesis-of-logics--how-to-cut-and-paste-reasoning-systems--applied-logic-series-
;; http://gigapedia.com/items/99492/philosophy-of-logic--handbook-of-the-philosophy-of-science-
;; http://gigapedia.com/items/104047/the-rise-of-modern-logic--from-leibniz-to-frege--volume-3--handbook-of-the-history-of-logic-
;; http://gigapedia.com/items/129108/interactive-logic--selected-papers-from-the-7th-augustus-de-morgan-workshop--london--aup---texts-in-logic-and-games-
;; http://gigapedia.com/items/62180/handbook-of-philosophical-logic--volume-9--2nd-edition
;; http://gigapedia.com/items/68348/handbook-of-philosophical-logic--volume-7--2nd-edition
;; http://gigapedia.com/items/68349/handbook-of-philosophical-logic--volume-8---2nd-edition
;; http://gigapedia.com/items/68350/handbook-of-philosophical-logic--volume-6---2nd-edition
;; http://gigapedia.com/items/68351/handbook-of-philosophical-logic--volume-5--2nd-edition
;; http://gigapedia.com/items/68352/handbook-of-philosophical-logic--volume-4--2nd-edition
;; http://gigapedia.com/items/68353/handbook-of-philosophical-logic--volume-3--2nd-edition
;; http://gigapedia.com/items/68354/handbook-of-philosophical-logic--volume-2--2nd-edition
;; http://gigapedia.com/items/69515/mathematical-problems-from-applied-logic-ii--logics-for-the-xxist-century--international-mathematical-series-
;; http://gigapedia.com/items/373805/logic--methodology-and-philosophy-of-science-iv--proceedings-of-the-4th-international-congress-for-logic--methodology--and-philosophy-of-science--bucharest--1971--studies-in-logic-and-the-foundations-of-mathematics--volume-74-



;; http://gigapedia.com/items/121856/analyses-of-aristotle--jaakko-hintikka-selected-papers-
;; http://gigapedia.com/items/104031/game-theoretical-semantics--essays-on-semantics-by-hintikka--carlson--peacocke--rantala-and-saarinen--studies-in-linguistics-and-philosophy-
;; http://gigapedia.com/items/105325/on-godel--wadsworth-philosophers-series-
;; http://gigapedia.com/items/84785/logic-for-computer-science---foundations-of-automatic-theorem-proving
;; http://search.gigapedia.com/?q=recursion

;; http://www.amazon.co.uk/Intuitionistic-Type-Theory-Giovanni-Lectures/dp/8870881059/ref=sr_1_4?ie=UTF8&s=books&qid=1263997364&sr=1-4

;; http://gigapedia.com/items/275307/foundations-without-foundationalism--a-case-for-second-order-logic--oxford-logic-guides-


;; Download these:
;;   http://gigapedia.com/items/223615/a-course-in-mathematical-logic
;;   http://gigapedia.com/items/108160/lectures-on-non--standard-analysis--lecture-notes-in-mathematics-

;; http://www.eecs.harvard.edu/shieber/Biblio/
;; http://gigapedia.com/items/376162/constraint-based-grammar-formalisms--parsing-and-type-inference-for-natural-and-computer-languages
;; http://gigapedia.com/items/5210/prolog-and-natural-language-analysis--center-for-the-study-of-language-and-information---lecture-notes-












;;
;; Local Variables:
;; mode:   emacs-lisp
;; coding: raw-text-unix
;; End: