Tools

LEADER 03794cam a22005297a 4500

001 ssj0000535291;

003 WaSeSS;

005 20240412080346.0;

006 m d ;

007 cr n ;

008 110711s2011 enk sb 001 0 eng d;

010 a| 2011934034;

016 7 a| 0159656232| Uk;

020 a| 9780857298072 (hbk. : alk. paper);

020 a| 0857298070 (hbk. : alk. paper);

020 z| 9780857298089 (e-book);

020 z| 0857298089 (e-book);

035 a| (WaSeSS)ssj0000535291;

042 a| lccopycat;

049 a| EREEa| NEHH;

050 00 a| QA248b| .S364 2011;

100 1 a| Schwartz, Jacob T.=| ^A16632;

245 10 a| Computational logic and set theoryh| [electronic resource] :b| applying formalized logic to analysis /c| Jacob T. Schwartz, Domenico Cantone, Eugenio G. Omodeo.;

246 30 a| Applying formalized logic to analysis;

260 a| London ;a| New York :b| Springer,;

300 a| xvii, 416 p. ;c| 24 cm.;

504 a| Includes bibliographical references and index.;

505 0 a| Introduction -- Propositional- and predicate-calculus preliminaries -- A survey of inference mechanisms -- More on the structure of the verifier system -- A closer examination of the sequence of definitions and theorems presented in this book -- Undecidability and unsolvability -- A self-contained beginning for Ref's main proof scenario.;

506 a| Available only to authorized users.;

520 a| As computer software becomes more complex, the question of how its correctness can be assured grows ever more critical. Formal logic embodied in computer programs is an important part of the answer to this problem. This must-read text presents the pioneering work of the late Professor Jacob (Jack) T. Schwartz on computational logic and set theory and its application to proof verification techniques, culminating in the ÆtnaNova system, a prototype computer program designed to verify the correctness of mathematical proofs presented in the language of set theory. Taking a systematic approach, the book begins with a survey of traditional branches of logic before describing in detail the underlying design of the ÆtnaNova system. Major classical results on undecidability and unsolvability are then recast for this system. Readers do not require great knowledge of formal logic in order to follow the text, but a good understanding of standard programming techniques, and a familiarity with mathematical definitions and proofs reflecting the usual levels of rigor is assumed.;

538 a| Mode of access: World Wide Web;

650 0 a| Set theory.=| ^A26682;

655 0 a| Electronic books.=| ^A491897;

700 1 a| Cantone, Domenico.?| UNAUTHORIZED;

700 1 a| Omodeo, Eugenio.?| UNAUTHORIZED;

856 40 z| Full text available from Springer Booksu| https://go.openathens.net/redirector/ecu.edu?url=https%3A%2F%2Flink.springer.com%2F10.1007%2F978-0-85729-808-9;

856 40 z| Full text available from Springer Nature - Springer Computer Science eBooks 2011 English Internationalu| https://go.openathens.net/redirector/ecu.edu?url=https%3A%2F%2Flink.springer.com%2F10.1007%2F978-0-85729-808-9;

947 a| (OCoLC)ocn733239376;

949 a| CLICK ON WEB ADDRESSw| ASISh| JOYNER188;

949 a| CLICK ON WEB ADDRESSw| ASISh| HSL77;

949 a| CLICK ON WEB ADDRESSw| ASISh| JMUSIC60;

596 a| 1 3 4;

998 a| 4023889;

999 a| CLICK ON WEB ADDRESSw| ASISc| 1i| 4023889-1001l| JNETm| JOYNERr| Ys| Yt| JNESSBKu| 1/1/2016x| EBOOKz| JERESOURCE;

999 a| CLICK ON WEB ADDRESSw| ASISc| 1i| 4023889-2001l| HSLELECm| HSLr| Ys| Yt| HEBKu| 1/1/2016x| EBOOKz| HERESOURCE;

999 a| CLICK ON WEB ADDRESSw| ASISc| 1i| 4023889-3001l| MNETm| JMUSICr| Ys| Yt| MNESSBKu| 1/1/2016x| EBOOKz| JERESOURCE;

Computational logic and set theory applying formalized logic to analysis / Jacob T. Schwartz, Domenico Cantone, Eugenio G. Omodeo.

Author/creator	Schwartz, Jacob T.
Other author	Cantone, Domenico.
Other author	Omodeo, Eugenio.
Format	Electronic
Publication Info	London ; New York : Springer,
Description	xvii, 416 p. ; 24 cm.
Supplemental Content	Full text available from Springer Books
Supplemental Content	Full text available from Springer Nature - Springer Computer Science eBooks 2011 English International
Subjects	Set theory.

Portion of title	Applying formalized logic to analysis
Contents	Introduction -- Propositional- and predicate-calculus preliminaries -- A survey of inference mechanisms -- More on the structure of the verifier system -- A closer examination of the sequence of definitions and theorems presented in this book -- Undecidability and unsolvability -- A self-contained beginning for Ref's main proof scenario.
Abstract	As computer software becomes more complex, the question of how its correctness can be assured grows ever more critical. Formal logic embodied in computer programs is an important part of the answer to this problem. This must-read text presents the pioneering work of the late Professor Jacob (Jack) T. Schwartz on computational logic and set theory and its application to proof verification techniques, culminating in the ÆtnaNova system, a prototype computer program designed to verify the correctness of mathematical proofs presented in the language of set theory. Taking a systematic approach, the book begins with a survey of traditional branches of logic before describing in detail the underlying design of the ÆtnaNova system. Major classical results on undecidability and unsolvability are then recast for this system. Readers do not require great knowledge of formal logic in order to follow the text, but a good understanding of standard programming techniques, and a familiarity with mathematical definitions and proofs reflecting the usual levels of rigor is assumed.
Bibliography note	Includes bibliographical references and index.
Access restriction	Available only to authorized users.
Technical details	Mode of access: World Wide Web
Genre/form	Electronic books.
LCCN	2011934034
ISBN	9780857298072 (hbk. : alk. paper)
ISBN	0857298070 (hbk. : alk. paper)

Availability

Library	Location	Call Number	Status	Item Actions
	Electronic Resources	Access Content Online	✔ Available

Computational logic and set theory applying formalized logic to analysis / Jacob T. Schwartz, Domenico Cantone, Eugenio G. Omodeo.

Click here for more information about this title

Availability