| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996387422503316 |
|
|
Autore |
Foster Samuel <d. 1652.> |
|
|
Titolo |
The art of dialling, by a new, easie, and most speedy way [[electronic resource] ] : Shewing how to describe the hour lines upon all forts of plains; howsoever, or in what latitude soever situated. Also; to find the hour of the day, and the azimuth of the sun, whereby the sight of any plain is examined. Performed by a quadrant filled with lines necessary to that purpose. / / Invented and published in Anno 1638, by Samuel Forster, then Professor of Astronomie in Gresham Colledge |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
London, : Printed by J. R. for Francis Eglesfield at the Marygold in St. Pauls Churchyard, 1675 |
|
|
|
|
|
|
|
|
|
Edizione |
[The second edition /] |
|
|
|
|
|
Descrizione fisica |
|
[8], 55, [1] p., [1] leaf of plates : ill., charts |
|
|
|
|
|
|
Altri autori (Persone) |
|
LeybournWilliam <1626-1716.> |
|
|
|
|
|
|
Soggetti |
|
Time measurements |
Quadrant |
Latitude |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Reproduction of the original in the National Library of Scotland. |
|
|
|
|
|
|
Sommario/riassunto |
|
|
|
|
|
|
|
|
|
|
|
|
|
2. |
Record Nr. |
UNINA9910767560303321 |
|
|
Titolo |
Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2000 St Andrews, Scotland, UK, July 3-7, 2000 Proceedings / / edited by Roy Dyckhoff |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2000.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (X, 440 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Artificial Intelligence ; ; 1847 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Artificial intelligence |
Programming languages (Electronic computers) |
Logic, Symbolic and mathematical |
Artificial Intelligence |
Programming Languages, Compilers, Interpreters |
Mathematical Logic and Formal Languages |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references. |
|
|
|
|
|
|
Nota di contenuto |
|
Invited Lectures -- Tableau Algorithms for Description Logics -- Modality and Databases -- Local Symmetries in Propositional Logic -- Comparison -- Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison -- Consistency Testing: The RACE Experience -- Benchmark Analysis with FaCT -- MSPASS: Modal Reasoning by Translation and First-Order Resolution -- TANCS-2000 Results for DLP -- Evaluating *SAT on TANCS 2000 Benchmarks -- Research Papers -- A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations -- A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus -- An Analytic Calculus for Quantified Propositional Gödel Logic -- A Tableau Method for Inconsistency-Adaptive Logics -- A Tableau Calculus for Integrating First-Order and Elementary Set Theory Reasoning -- Hypertableau and Path-Hypertableau Calculi for some Families of Intermediate Logics -- Variants of First-Order Modal Logics -- Complexity of Simple Dependent Bimodal Logics -- Properties of Embeddings from Int to S4 |
|
|
|
|
|
|
|
|
|
|
|
-- Term-Modal Logics -- A Subset-Matching Size-Bounded Cache for Satisfiability in Modal Logics -- Dual Intuitionistic Logic Revisited -- Model Sets in a Nonconstructive Logic of Partial Terms with Definite Descriptions -- Search Space Compression in Connection Tableau Calculi Using Disjunctive Constraints -- Matrix-Based Inductive Theorem Proving -- Monotonic Preorders for Free Variable Tableaux -- The Mosaic Method for Temporal Logics -- Sequent-Like Tableau Systems with the Analytic Superformula Property for the Modal Logics KB, KDB, K5, KD5 -- A Tableau Calculus for Equilibrium Entailment -- Towards Tableau-Based Decision Procedures for Non-Well-Founded Fragments of Set Theory -- Tableau Calculus for Only Knowing and Knowing At Most -- A Tableau-Like Representation Framework for Efficient Proof Reconstruction -- The Semantic Tableaux Version of the Second Incompleteness Theorem Extends Almost to Robinson’s Arithmetic Q -- System Descriptions -- Redundancy-Free Lemmatization in the Automated Model-Elimination Theorem Prover AI-SETHEO -- E-SETHEO: An Automated3 Theorem Prover. |
|
|
|
|
|
|
Sommario/riassunto |
|
This book constitutes the refereed proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2000, held in St Andrews, Scotland, UK, in July 2000.The 23 revised full papers and 2 system descriptions presented were carefully reviewed and selected from 42 submissions. Also included are 3 invited lectures and 6 nonclassical system comparisons. All current issues surrounding the mechanization of reasoning with tableaux and similar methods are addressed - ranging from theoretical foundations to implementation, systems development, and applications, as well as covering a broad variety of logical calculi. |
|
|
|
|
|
|
|
| |