Automated reasoning : First International Joint Conference, IJCAR 2001, Siena, Italy, June 18 22, 2001 : proceedings

Shranjeno v:
Bibliografske podrobnosti
Korporativna značnica: International Joint Conference on Automated Reasoning :Sienne, Italie
Drugi avtorji: Goré, Rajeev (Directeur de la publication), Leitsch, Alexander, 1952- (Directeur de la publication), Nipkow, Tobias, 1958-..., informaticien (Directeur de la publication)
Format: Livre numérique
Jezik:Anglais
Izdano: Berlin [etc.] : Springer [20..].
Cham : Springer Nature
Serija:Lecture notes in computer science. Lecture notes in artificial intelligence 2083
Teme:
Online dostop:Accès sur la plateforme de l'éditeur
Accès sur la plateforme Istex
Accès Université d'Orléans
Accès INSA CVL
Sporočilo: Archives Springer e-books (Licence nationale)
Archives Springer e-books (Licence nationale)
Autres localisations: Voir dans le Sudoc
Edition sous un autre format:• Automated reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, proceedings, Rajeev Goré, Alexander Leitsch, Tobias Nipkow (eds.), 2001, New York, Springer, 1 vol. (XV-708 p.), Lecture notes in computer science, 3-540-42254-4
• Automated Reasoning, Texte imprimé, 9783662171196
LEADER 07931nam a22004337a 4500
001 949406
008 110927q2000 xxe ||| |||| 00| 0 eng d
009 PPN155236768
020 |a 9783540457442 (PDF) 
041 0 |a eng 
082 |a 004 
111 2 |a International Joint Conference on Automated Reasoning  |n (01  |d  :2001  |c  :Sienne, Italie). 
245 1 0 |a Automated reasoning :  |b First International Joint Conference, IJCAR 2001, Siena, Italy, June 18 22, 2001 : proceedings   |c [edited by] Rajeev Goré, Alexander Leitsch, Tobias Nipkow. 
260 |a Berlin [etc.] :  |b Springer. 
260 |a Cham :  |b Springer Nature,  |c [20..]. 
490 0 |a Lecture notes in computer science. Lecture notes in artificial intelligence  |v 2083  |x 1611-3349  |x 2945-9141 
500 |a Archives Springer e-books (Licence nationale) 
500 |a Archives Springer e-books (Licence nationale) 
505 0 |a Invited Talks -- Program Termination Analysis by Size-Change Graphs (Abstract) -- SET Cardholder Registration: The Secrecy Proofs -- SET Cardholder Registration: The Secrecy Proofs -- Algorithms, Datastructures, and other Issues in Efficient Automated Deduction -- Algorithms, Datastructures, and other Issues in Efficient Automated Deduction -- Description, Modal and temporal Logics -- The Description Logic ALCNH R + Extended with Concrete Domains: A Practically Motivated Approach -- NExpTime-Complete Description Logics with Concrete Domains -- Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics -- Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics -- The Hybrid ?-Calculus -- The Hybrid ?-Calculus -- The Inverse Method Implements the Automata Approach for Modal Satisfiability -- The Inverse Method Implements the Automata Approach for Modal Satisfiability -- Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL -- Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL -- Tableaux for Temporal Description Logic with Constant Domains -- Tableaux for Temporal Description Logic with Constant Domains -- Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation -- Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation -- Saturation Based Theorem Proving, Applications, and Data Structures -- Instructing Equational Set-Reasoning with Otter -- NP-Completeness of Refutability by Literal-Once Resolution -- Ordered Resolution vs. Connection Graph resolution -- A Model-Based Completeness Proof of Extended Narrowing and Resolution -- A Model-Based Completeness Proof of Extended Narrowing and Resolution.-A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality -- A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality -- Superposition and Chaining for Totally Ordered Divisible Abelian Groups -- Superposition and Chaining for Totally Ordered Divisible Abelian Groups -- Context Trees -- Context Trees -- On the Evaluation of Indexing Techniques for Theorem Proving -- On the Evaluation of Indexing Techniques for Theorem Proving -- Logic Programming and Nonmonotonic Reasoning -- Preferred Extensions of Argumentation Frameworks: Query, Answering, and Computation -- Bunched Logic Programming -- A Top-Down Procedure for Disjunctive Well-Founded Semantics -- A Second-Order Theorem Prover Applied to Circumscription -- NoMoRe: A System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics -- NoMoRe: A System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics -- Propositional Satisfiability and Quantified Boolean Logic -- Conditional Pure Literal Graphs -- Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability -- QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability -- System Abstract: E 0.61 -- Vampire 1.1 -- DCTP - A Disconnection Calculus Theorem Prover - System Abstract -- DCTP - A Disconnection Calculus Theorem Prover - System Abstract -- Logical Frameworks, Higher-Order Logic, Interactive Theorem Proving -- More On Implicit Syntax -- Termination and Reduction Checking for Higher-Order Logic Programs -- P.rex: An Interactive Proof Explainer -- JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants -- Semantic Guidance -- The eXtended Least Number Heuristic -- System Description: SCOTT-5 -- Combination of Distributed Search and Multi-Search in Peers-mcd.d -- Lotrec: The Generic Tableau Prover for Modal and Description Logics -- The modprof Theorem Prover -- A New System and Methodology for Generating Random Modal Formulae -- Equational Theorem Proving and Term Rewriting -- Decidable Classes of Inductive Theorems -- Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems -- Decidability and Complexity of Finitely Closable Linear Equational Theories -- A New Meta-Complexity Theorem for Bottom-Up Logic Programs -- Tableau, Sequent, Natural Deduction Calculi and Proof Theory -- Canonical Propositional Gentzen-Type Systems -- Incremental Closure of Free Variable Tableaux -- Deriving Modular Programs from Short Proofs -- A General Method for Using Schematizations in Automated Deduction -- Automata, Specification, Verification, and Logics of Programs -- Approximating Dependency Graphs Using Tree Automata Techniques -- On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables -- A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities -- Flaw Detection in Formal Specifications -- CCE: Testing Ground Joinability -- System Description: RDL Rewrite and Decision Procedure Laboratory -- lolliCoP A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic -- Nonclassical Logics -- Muscadet 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction -- Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory -- STRIP: Structural Sharing for Efficient Proof-Search -- RACER System Description. 
506 |a Accès en ligne pour les établissements français bénéficiaires des licences nationales 
506 |a Accès soumis à abonnement pour tout autre établissement 
506 |a Conditions particulières de réutilisation pour les bénéficiaires des licences nationales. https://www.licencesnationales.fr/springer-nature-ebooks-contrat-licence-ln-2017 
650 |a Génie logiciel 
650 |a Informatique 
650 |a Intelligence artificielle 
650 |a Logique symbolique et mathématique 
650 |a Théorèmes  |x Démonstration automatique 
650 |a Logique informatique 
650 |a Actes de congrès 
700 1 |a Goré, Rajeev.  |4 pbd 
700 1 |a Leitsch, Alexander,  |d 1952-  |4 pbd 
700 1 |a Nipkow, Tobias,  |d 1958-...,  |c informaticien.  |4 pbd 
776 0 |0 057845824  |t Automated reasoning  |o First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001  |o proceedings  |f Rajeev Goré, Alexander Leitsch, Tobias Nipkow (eds.)  |d 2001  |c New York  |n Springer  |p 1 vol. (XV-708 p.)  |s Lecture notes in computer science  |z 3-540-42254-4 
776 0 |t Automated Reasoning  |b Texte imprimé  |z 9783662171196 
856 4 |q PDF  |u https://doi.org/10.1007/3-540-45744-5  |z Accès sur la plateforme de l'éditeur 
856 4 |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-RL4HKG8C-V  |z Accès sur la plateforme Istex 
856 4 |5 452349901:748059946  |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-45744-5  |z Accès Université d'Orléans 
856 4 |5 180339901:751511455  |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-45744-5  |z Accès INSA CVL 
997 |0 949406  |1 Livre numérique  |a Ressource numérique  |b INSA  |b ENSA  |c 0/Bibliothèque numérique/  |c 1/Bibliothèque numérique/Autre ressource numérique/