Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Automated Reasoning [[electronic resource] ] : 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings / / edited by Didier Galmiche, Stephan Schulz, Roberto Sebastiani
| Automated Reasoning [[electronic resource] ] : 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings / / edited by Didier Galmiche, Stephan Schulz, Roberto Sebastiani |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XVI, 724 p. 128 illus.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Mathematical logic
Artificial intelligence Computer logic Algorithms Software engineering Programming languages (Electronic computers) Mathematical Logic and Formal Languages Artificial Intelligence Logics and Meanings of Programs Algorithm Analysis and Problem Complexity Software Engineering Programming Languages, Compilers, Interpreters |
| ISBN | 3-319-94205-0 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem -- FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics -- Superposition for Lambda-Free Higher-Order Logic -- Automated Reasoning about Key Sets -- A Tableaux Calculus for Reducing Proof Size -- FORT 2.0 -- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover -- The Higher-Order Prover Leo-III -- Well-Founded Unions -- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories -- Cubicle-W: Parameterized Model Checking on Weak Memory -- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property -- A Why3 framework for reflection proofs and its application to GMP's algorithms -- Infinitely-valued Logic -- Uniform Substitution for Differential Game Logic -- A Logical Framework with Commutative and Non-Commutative Subexponentials -- Exploring Approximations for Floating-Point Arithmetic using UppSAT -- Complexity of Combinations of Qualitative Constraint Satisfaction Problems -- A Generic Framework for Implicate Generation Modulo Theories -- A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems -- A New Probabilistic Algorithm for Approximate Model Counting -- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems -- Cops and CoCoWeb: Infrastructure for Conuence Tools -- Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing -- Superposition with Datatypes and Codatatypes -- Efficient encodings of first-order Horn formulas in equational logic -- A FOOLish Encoding of the Next State Relations of Imperative Programs -- Constructive Decision via Redundancy-free Proof-Search -- Deciding the First-Order Theory of an Algebra of Feature Trees with Updates -- A Separation Logic with Data: Small Models and Automation -- MaedMax: A Maximal Ordered Completion Tool -- From Syntactic Proofs to Combinatorial Proofs -- A Resolution-Based Calculus for Preferential Logics -- Extended Resolution Simulates DRAT -- Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle -- Efficient Interpolation for the Theory of Arrays -- ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback -- Theories as Types -- Datatypes with Shared Selectors -- Enumerating Justifications using Resolution -- A SAT-Based Approach to Learn Explainable Decision Sets -- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions -- An abstraction-refinement framework for reasoning with large theories -- Efficient Model Construction for Horn Logic with VLog: System Description -- Focussing, MALL and the polynomial hierarchy -- Checking Array Bounds by Abstract Interpretation and Symbolic Expressions. |
| Record Nr. | UNINA-9910349422303321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Reasoning [[electronic resource] ] : 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings / / edited by Didier Galmiche, Stephan Schulz, Roberto Sebastiani
| Automated Reasoning [[electronic resource] ] : 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings / / edited by Didier Galmiche, Stephan Schulz, Roberto Sebastiani |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XVI, 724 p. 128 illus.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Mathematical logic
Artificial intelligence Computer logic Algorithms Software engineering Programming languages (Electronic computers) Mathematical Logic and Formal Languages Artificial Intelligence Logics and Meanings of Programs Algorithm Analysis and Problem Complexity Software Engineering Programming Languages, Compilers, Interpreters |
| ISBN | 3-319-94205-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem -- FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics -- Superposition for Lambda-Free Higher-Order Logic -- Automated Reasoning about Key Sets -- A Tableaux Calculus for Reducing Proof Size -- FORT 2.0 -- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover -- The Higher-Order Prover Leo-III -- Well-Founded Unions -- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories -- Cubicle-W: Parameterized Model Checking on Weak Memory -- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property -- A Why3 framework for reflection proofs and its application to GMP's algorithms -- Infinitely-valued Logic -- Uniform Substitution for Differential Game Logic -- A Logical Framework with Commutative and Non-Commutative Subexponentials -- Exploring Approximations for Floating-Point Arithmetic using UppSAT -- Complexity of Combinations of Qualitative Constraint Satisfaction Problems -- A Generic Framework for Implicate Generation Modulo Theories -- A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems -- A New Probabilistic Algorithm for Approximate Model Counting -- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems -- Cops and CoCoWeb: Infrastructure for Conuence Tools -- Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing -- Superposition with Datatypes and Codatatypes -- Efficient encodings of first-order Horn formulas in equational logic -- A FOOLish Encoding of the Next State Relations of Imperative Programs -- Constructive Decision via Redundancy-free Proof-Search -- Deciding the First-Order Theory of an Algebra of Feature Trees with Updates -- A Separation Logic with Data: Small Models and Automation -- MaedMax: A Maximal Ordered Completion Tool -- From Syntactic Proofs to Combinatorial Proofs -- A Resolution-Based Calculus for Preferential Logics -- Extended Resolution Simulates DRAT -- Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle -- Efficient Interpolation for the Theory of Arrays -- ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback -- Theories as Types -- Datatypes with Shared Selectors -- Enumerating Justifications using Resolution -- A SAT-Based Approach to Learn Explainable Decision Sets -- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions -- An abstraction-refinement framework for reasoning with large theories -- Efficient Model Construction for Horn Logic with VLog: System Description -- Focussing, MALL and the polynomial hierarchy -- Checking Array Bounds by Abstract Interpretation and Symbolic Expressions. |
| Record Nr. | UNISA-996466437703316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : 22nd International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Proceedings / / edited by Didier Galmiche, Dominique Larchey-Wendling
| Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : 22nd International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Proceedings / / edited by Didier Galmiche, Dominique Larchey-Wendling |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (X, 289 p. 34 illus.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Mathematical logic Computer programming Software engineering Computer science—Mathematics Computer logic Artificial Intelligence Mathematical Logic and Formal Languages Programming Techniques Software Engineering Discrete Mathematics in Computer Science Logics and Meanings of Programs |
| ISBN | 3-642-40537-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Witness Runs for Counter Machines (Abstract) -- On the Duality of Proofs and Countermodels in Labelled Sequent Calculi -- A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions -- Research Papers -- Dealing with Symmetries in Modal Tableaux -- Tableaux for Verification of Data-Centric Processes -- Bounded Proofs and Step Frames -- Compression of Propositional Resolution Proofs by Lowering Subproofs -- A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: An Implementation -- Hypersequent and Labelled Calculi for Intermediate Logics -- TATL: Implementation of ATL Tableau-Based Decision Procedure -- A Terminating Evaluation-Driven Variant of G3i -- Model Checking General Linear Temporal Logic -- Semantically Guided Evolution of SHI ABoxes -- Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture -- Understanding Resolution Proofs through Herbrand’s Theorem -- A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search -- A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI -- Prefixed Tableau Systems for Logic of Proofs and Provability -- Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5 -- Schemata of Formulæ in the Theory of Arrays -- TAFA – A Tool for Admissibility in Finite Algebras -- Formalizing Cut Elimination of Coalgebraic Logics in Coq -- Intelligent Tableau Algorithm for DL Reasoning. |
| Record Nr. | UNISA-996466061703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : 22nd International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Proceedings / / edited by Didier Galmiche, Dominique Larchey-Wendling
| Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : 22nd International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Proceedings / / edited by Didier Galmiche, Dominique Larchey-Wendling |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (X, 289 p. 34 illus.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Mathematical logic Computer programming Software engineering Computer science—Mathematics Computer logic Artificial Intelligence Mathematical Logic and Formal Languages Programming Techniques Software Engineering Discrete Mathematics in Computer Science Logics and Meanings of Programs |
| ISBN | 3-642-40537-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Witness Runs for Counter Machines (Abstract) -- On the Duality of Proofs and Countermodels in Labelled Sequent Calculi -- A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions -- Research Papers -- Dealing with Symmetries in Modal Tableaux -- Tableaux for Verification of Data-Centric Processes -- Bounded Proofs and Step Frames -- Compression of Propositional Resolution Proofs by Lowering Subproofs -- A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: An Implementation -- Hypersequent and Labelled Calculi for Intermediate Logics -- TATL: Implementation of ATL Tableau-Based Decision Procedure -- A Terminating Evaluation-Driven Variant of G3i -- Model Checking General Linear Temporal Logic -- Semantically Guided Evolution of SHI ABoxes -- Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture -- Understanding Resolution Proofs through Herbrand’s Theorem -- A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search -- A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI -- Prefixed Tableau Systems for Logic of Proofs and Provability -- Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5 -- Schemata of Formulæ in the Theory of Arrays -- TAFA – A Tool for Admissibility in Finite Algebras -- Formalizing Cut Elimination of Coalgebraic Logics in Coq -- Intelligent Tableau Algorithm for DL Reasoning. |
| Record Nr. | UNINA-9910484152303321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : International Conference, TABLEAUX'97, Pont-a-Mousson, France, May 13-16, 1997 Proceedings / / edited by Didier Galmiche
| Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : International Conference, TABLEAUX'97, Pont-a-Mousson, France, May 13-16, 1997 Proceedings / / edited by Didier Galmiche |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (XII, 380 p.) |
| Disciplina | 006.3/33 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Architecture, Computer
Artificial intelligence Mathematical logic Computer System Implementation Artificial Intelligence Mathematical Logic and Formal Languages Mathematical Logic and Foundations |
| ISBN | 3-540-69046-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | MGTP: A model generation theorem prover — Its advanced features and applications — -- Three faces of natural deduction -- Tableaux for logic programming with strong negation -- Generalized tableau systems for intermediate propositional logics -- Lean induction principles for tableaux -- Tableaux for diagnosis applications -- Free variable tableaux for propositional modal logics -- A sequent calculus for skeptical Default Logic -- A fast saturation strategy for set-theoretic tableaux -- Hintikka multiplicities in matrix decision methods for some propositional modal logics -- Automated natural deduction prover and experiments -- Non-elementary speed-ups in proof length by different variants of classical analytic calculi -- Ordered tableaux: Extensions and applications -- Two loop detection mechanisms: A comparison -- Subgoal alternation in model elimination -- Projection: A unification procedure for tableaux in Conceptual Graphs -- On quasitautologies -- Tableaux methods for access control in distributed systems -- Proving correctness of labeled transition systems by semantic tableaux -- Tableau methods for PA-processes -- A tableau proof system for a mazurkiewicz trace logic with fixpoints -- ileanTAP: An intuitionistic theorem prover -- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models -- A framework for using knowledge in tableau proofs -- A sequent calculus for reasoning in four-valued Description Logics -- Tableaux for functional dependencies and independencies. |
| Record Nr. | UNISA-996465546903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : International Conference, TABLEAUX'97, Pont-a-Mousson, France, May 13-16, 1997 Proceedings / / edited by Didier Galmiche
| Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : International Conference, TABLEAUX'97, Pont-a-Mousson, France, May 13-16, 1997 Proceedings / / edited by Didier Galmiche |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (XII, 380 p.) |
| Disciplina | 006.3/33 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Architecture, Computer
Artificial intelligence Mathematical logic Computer System Implementation Artificial Intelligence Mathematical Logic and Formal Languages Mathematical Logic and Foundations |
| ISBN | 3-540-69046-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | MGTP: A model generation theorem prover — Its advanced features and applications — -- Three faces of natural deduction -- Tableaux for logic programming with strong negation -- Generalized tableau systems for intermediate propositional logics -- Lean induction principles for tableaux -- Tableaux for diagnosis applications -- Free variable tableaux for propositional modal logics -- A sequent calculus for skeptical Default Logic -- A fast saturation strategy for set-theoretic tableaux -- Hintikka multiplicities in matrix decision methods for some propositional modal logics -- Automated natural deduction prover and experiments -- Non-elementary speed-ups in proof length by different variants of classical analytic calculi -- Ordered tableaux: Extensions and applications -- Two loop detection mechanisms: A comparison -- Subgoal alternation in model elimination -- Projection: A unification procedure for tableaux in Conceptual Graphs -- On quasitautologies -- Tableaux methods for access control in distributed systems -- Proving correctness of labeled transition systems by semantic tableaux -- Tableau methods for PA-processes -- A tableau proof system for a mazurkiewicz trace logic with fixpoints -- ileanTAP: An intuitionistic theorem prover -- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models -- A framework for using knowledge in tableau proofs -- A sequent calculus for reasoning in four-valued Description Logics -- Tableaux for functional dependencies and independencies. |
| Record Nr. | UNINA-9910768459603321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||