دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1 نویسندگان: Peter B. Andrews (auth.), Jörg H. Siekmann (eds.) سری: Lecture Notes in Computer Science 230 ISBN (شابک) : 9783540167808, 9783540398615 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 1986 تعداد صفحات: 717 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 15 مگابایت
کلمات کلیدی مربوط به کتاب هشتمین کنفرانس بین المللی کسر خودکار: آکسفورد ، انگلیس ، 27 ژوئیه تا 1 آگوست 1986 مجموعه مقالات: منطق ریاضی و زبان های رسمی، هوش مصنوعی (شامل رباتیک)
در صورت تبدیل فایل کتاب 8th International Conference on Automated Deduction: Oxford, England, July 27–August 1, 1986 Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب هشتمین کنفرانس بین المللی کسر خودکار: آکسفورد ، انگلیس ، 27 ژوئیه تا 1 آگوست 1986 مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
Connections and higher-order logic....Pages 1-4
Commutation, transformation, and termination....Pages 5-20
Full-commutation and fair-termination in equational (and combined) term-rewriting systems....Pages 21-41
An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations....Pages 42-51
Proving termination of associative commutative rewriting systems by rewriting....Pages 52-61
Relating resolution and algebraic completion for Horn logic....Pages 62-78
A simple non-termination test for the Knuth-Bendix method....Pages 79-88
A new formula for the execution of categorical combinators....Pages 89-98
Proof by induction using test sets....Pages 99-117
How to prove equivalence of term rewriting systems without induction....Pages 118-127
Sufficient completeness, term rewriting systems and ”anti-unification”....Pages 128-140
A new method for establishing refutational completeness in theorem proving....Pages 141-152
A theory of diagnosis from first principles....Pages 153-153
Some contributions to the logical analysis of circumscription....Pages 154-171
Modal theorem proving....Pages 172-189
Computational aspects of three-valued logic....Pages 190-198
Resolution and quantified epistemic logics....Pages 199-208
A commonsense theory of nonmonotonic reasoning....Pages 209-228
Negative paramodulation....Pages 229-239
The heuristics and experimental results of a new hyperparamodulation: HL -resolution....Pages 240-253
ECR: An equality conditional resolution proof procedure....Pages 254-271
Using narrowing to do isolation in symbolic equation solving — an experiment in automated reasoning....Pages 272-280
Formulation of induction formulas in verification of prolog programs....Pages 281-299
Program verifier \"Tatzelwurm\": Reasoning about systems systems of linear inequalities....Pages 300-305
An interactive verification system based on dynamic logic....Pages 306-315
What you always wanted to know about clause graph resolution....Pages 316-336
Parallel theorem proving with connection graphs....Pages 337-352
Theory links in semantic graphs....Pages 353-364
Abstraction using generalization functions....Pages 365-376
An improvement of deduction plans: Refutation plans....Pages 377-383
Controlling deduction with proof condensation and heuristics....Pages 384-393
Nested resolution....Pages 394-402
Mechanizing constructive proofs....Pages 403-403
Implementing number theory: An experiment with Nuprl....Pages 404-415
Parallel algorithms for term matching....Pages 416-430
Unification in combinations of collapse-free theories with disjoint sets of function symbols....Pages 431-449
Combination of unification algorithms....Pages 450-469
Unification in the data structure sets....Pages 470-488
NP-completeness of the set unification and matching problems....Pages 489-495
Matching with distributivity....Pages 496-505
Unification in boolean rings....Pages 506-513
Some relationships between unification, restricted unification, and matching....Pages 514-524
A classification of many-sorted unification problems....Pages 525-537
Unification in many-sorted equational theories....Pages 538-552
Classes of first order formulas under various satisfiability definitions....Pages 553-563
Diamond formulas in the dynamic logic of recursively enumerable programs....Pages 564-571
A prolog machine....Pages 572-572
A prolog technology theorem prover: Implementation by an extended prolog compiler....Pages 573-587
Paths to high-performance automated theorem proving....Pages 588-597
Purely functional implementation of a logic....Pages 598-607
Causes for events: Their computation and applications....Pages 608-621
How to clear a block: Plan formation in situational logic....Pages 622-640
Deductive synthesis of sorting programs....Pages 641-660
The TPS theorem proving system....Pages 661-664
Trspec: A term rewriting based system for algebraic specifications....Pages 665-667
Highly parallel inference machine....Pages 668-669
Automatic theorem proving in the ISDV system....Pages 670-671
The karlsruhe induction theorem proving system....Pages 672-674
Overview of a theorem-prover for a computational logic....Pages 675-678
GEO-prover — A geometry theorem prover developed at UT....Pages 679-680
The markgraf karl refutation procedure (MKRP)....Pages 681-682
The J-machine: Functional programming with combinators....Pages 683-684
The illinois prover: A general purpose resolution theorem prover....Pages 685-686
Theorem proving systems of the Formel project....Pages 687-688
The passau RAP system: Prototyping algebraic specifications using conditional narrowing....Pages 689-690
RRL: A rewrite rule laboratory....Pages 691-692
A geometry theorem prover based on Buchberger\'s algorithm....Pages 693-694
REVE a rewrite rule laboratory....Pages 695-696
ITP at argonne national laboratory....Pages 697-698
Autologic at university of victoria....Pages 699-700
Thinker....Pages 701-702
The KLAUS automated deduction system....Pages 703-704
The KRIPKE automated theorem proving system....Pages 705-706
SHD-prover at university of texas at austin....Pages 707-708