Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
45
views
15
references
Top references
cited by
4
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
3,175
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Recent Advances in AI Planning
Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS
other
Author(s):
Andrew Adams
,
Martin Dunstan
,
Hanne Gottliebsen
,
Tom Kelsey
,
Ursula Martin
,
Sam Owre
Publication date
(Online):
August 24 2001
Publisher:
Springer Berlin Heidelberg
Read this book at
Publisher
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
Numerical Algebra, Matrix Theory, Differential-Algebraic Equations, and Control Theory
Most cited references
15
Record
: found
Abstract
: not found
Article
: not found
REDLOG
Thomas Sturn
,
Andreas Dolzmann
(1997)
0
comments
Cited
37
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Book
: not found
Maple V Language Reference Manual
Bruce Char
,
Keith O. Geddes
,
Gaston H. Gonnet
…
(1991)
0
comments
Cited
33
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
The PROSPER Toolkit
Louise A. Dennis
,
Graham Collins
,
Michael Norrish
…
(2000)
0
comments
Cited
5
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2001
Publication date (Online):
August 24 2001
Pages
: 27-42
DOI:
10.1007/3-540-44755-5_4
SO-VID:
7dc0f2e7-c014-4310-bfdc-3f81a7834ebb
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 1
Supporting Storytelling in a Programming Environment for Middle School Children
pp. 1
Normative Multiagent Systems and Trust Dynamics
pp. 1
Interaction with Formal Mathematical Documents in Isabelle/PIDE
pp. 1
An Empirical Exploration of a Definition of Creative Novelty for Generative Art
pp. 1
Representing Social Structures in UML
pp. 3
BigKey: A Virtual Keyboard for Mobile Devices
pp. 3
Exploiting the Earth’s Spherical Geometry to Geolocate Images
pp. 20
Evolutionary Togetherness: How to Manage Coupled Evolution in Metamodeling Ecosystems
pp. 14
The IRIS Network of Excellence: Integrating Research in Interactive Storytelling
pp. 15
Case-Based Reasoning with Confidence
pp. 19
A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
pp. 25
On finding needles in WWW haystacks
pp. 25
Edutainment Robotics as Learning Tool
pp. 27
Analysis of RC4 and Proposal of Additional Layers for Better Security Margin
pp. 27
Efficient Use of Random Delays in Embedded Software
pp. 34
Efficient Selection of Time Samples for Higher-Order DPA with Projection Pursuits
pp. 27
Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS
pp. 37
Authoring Personalized Interactive Museum Stories
pp. 37
Formal Specification of Interaction in Agent Societies
pp. 40
Preimage Attacks on Full-ARIRANG: Analysis of DM-Mode with Middle Feed-Forward
pp. 42
Aporia – Exploring Continuation Desire in a Game Focused on Environmental Storytelling
pp. 44
Distributed Paillier Cryptosystem without Trusted Dealer
pp. 47
Waiting for Locks: How Long Does It Usually Take?
pp. 128
Simulation-Sound Arguments for LWE and Applications to KDM-CCA2 Security
pp. 14
Concurrent Semantics for the Web Services Specification Language DAML-S
pp. 35
Vision-Based Robot Localization Using Sporadic Features
pp. 43
Designing a Deontic Logic of Deadlines
pp. 47
Verified Bytecode Model Checkers
pp. 65
Blockchain Based Data Integrity Verification for Cloud Storage with T-Merkle Tree
pp. 69
Safety Case Impact Assessment in Automotive Software Systems: An Improved Model-Based Approach
pp. 85
Performance Analysis of a High-Level Abstractions-Based Hydrocode on Future Computing Systems
pp. 26
“I Want to Slay That Dragon!” - Influencing Choice in Interactive Storytelling
pp. 62
A Sentence Vector Based Over-Sampling Method for Imbalanced Emotion Classification
pp. 64
Explainable Recommendations in a Personalized Programming Practice System
pp. 68
A Taxonomy of Autonomy in Multiagent Organisation
pp. 78
Analysis of the Bitcoin UTXO Set
pp. 99
How to Make FDR Spin LTL Model Checking of CSP by Refinement
pp. 198
A survey of the logic of effective definitions
pp. 48
Transferring Game Mastering Laws to Interactive Digital Storytelling
pp. 71
Investigating the Characteristics and Research Impact of Sentiments in Tweets with Links to Computer Science Research Papers
pp. 87
Improved Known-Key Distinguishers on Feistel-SP Ciphers and Application to Camellia
pp. 108
A Prototype Proof Translator from HOL to Coq
pp. 127
Dispute Resolution in Accessible Voting Systems: The Design and Use of Audiotegrity
pp. 135
Impossible Differential Attack on Reduced Round SPARX-64/128
pp. 66
A Deductive Database with Datalog and SQL Query Languages
pp. 92
Concise Representations of Association Rules
pp. 97
SAT-Based Procedures for Temporal Reasoning
pp. 120
A Sound and Complete CPS-Translation for λμ-Calculus
pp. 143
Program specification and data refinement in type theory
pp. 162
Analysing Lock-Free Linearizable Datatypes Using CSP
pp. 97
Enhanced CAPTCHAs: Using Animation to Tell Humans and Computers Apart
pp. 103
Improving Touchscreen Accessibility in Self-Service Technology
pp. 122
On the Semantic Transparency of Visual Notations: Experiments with UML
pp. 129
Evolution of the McEliece Public Key Encryption Scheme
pp. 234
Universally Composable Direct Anonymous Attestation
pp. 248
Verifiable Delay Functions from Supersingular Isogenies and Pairings
pp. 119
Aligning Needles in a Haystack: Paraphrase Acquisition Across the Web
pp. 139
JavaSMT: A Unified Interface for SMT Solvers in Java
pp. 167
Yet Another Note on Block Withholding Attack on Bitcoin Mining Pools
pp. 179
Machine Learning Predictions for Underestimation of Job Runtime on HPC System
pp. 141
SPASS & FLOTTER version 0.42
pp. 148
Progress report on the disjunctive deductive database system dlv
pp. 320
Reusable Two-Round MPC from DDH
pp. 155
Towards a Digital Infrastructure for Illustrated Handwritten Archives
pp. 175
An extended VDM refinement relation
pp. 175
The Role of Data Integrity in EU Digital Signature Legislation — Achieving Statutory Trust for Sanitizable Signature Schemes
pp. 184
MQQ-SIG
pp. 203
ESM systems and the composition of their computations
pp. 209
Inverse Entailment in Nonmonotonic Logic Programs
pp. 101
Writing Interactive Fiction Scenarii with DraMachina
pp. 140
Interactive Cinema: Engagement and Interaction
pp. 183
Semantic Analysis Patterns
pp. 242
Induction and recursion on datatypes
pp. 173
Sorting and Recognizing Cheques and Financial Documents
pp. 197
The Improbable Differential Attack: Cryptanalysis of Reduced Round CLEFIA
pp. 203
The PERF Approach for Formal Verification
pp. 214
Group Signature with Constant Revocation Costs for Signers and Verifiers
pp. 240
A Lightweight Formal Analysis of a Multicast Key Management Scheme
pp. 241
Type classes in Haskell
pp. 248
Sound and complete forward and backward chainings of graph rules
pp. 245
TGV-Fusion
pp. 261
Formal Methods and Safety Certification: Challenges in the Railways Domain
pp. 188
Lifelong Learning Starting from Zero
pp. 242
The CMUnited-97 small robot team
pp. 245
Assessing Professional Cultural Differences Between Airline Pilots and Air Traffic Controllers
pp. 297
Two Lattice-Based Differential Fault Attacks Against ECDSA with wNAF Algorithm
pp. 202
Reading Again for the First Time: A Model of Rereading in Interactive Stories
pp. 250
Using UML for modeling complex real-time systems
pp. 269
Persuasive Design Strategy of Online Health Education for Elderly Adults Based on TAM Model
pp. 207
Service Provision in Ad Hoc Networks
pp. 226
Rectilinear Convex Hull with Minimum Area
pp. 245
Optimizing Student and Supervisor Interaction During the SciPro Thesis Process – Concepts and Design
pp. 293
Perceived Effectiveness, Credibility and Continuance Intention in E-commerce: A Study of Amazon
pp. 201
Impact of Expressive Wrinkles on Perception of a Virtual Character’s Facial Expressions of Emotions
pp. 332
Predicate Analysis with Block-Abstraction Memoization
pp. 345
Automatic Refinement Checking for B
pp. 355
Car or Public Transport—Two Worlds
pp. 254
Robust Dense Endoscopic Stereo Reconstruction for Minimally Invasive Surgery
pp. 316
What Decides the Dropout in MOOCs?
pp. 612
Analysis of SHA-512/224 and SHA-512/256
pp. 179
Rhetorical Coding of Health Promotion Dialogues
pp. 252
Tag Disambiguation through Flickr and Wikipedia
pp. 348
Formalizing a Language for Institutions and Norms
pp. 471
Cooperative Nets
pp. 244
Page Sets as Web Search Answers
pp. 356
Marlowe: Financial Contracts on Blockchain
pp. 434
Using VDM with rely and guarantee-conditions
pp. 579
A More Cautious Approach to Security Against Mass Surveillance
pp. 282
Designing for Compliance: Norms and Goals
pp. 387
Overview of LifeCLEF 2019: Identification of Amazonian Plants, South & North American Birds, and Niche Prediction
pp. 293
Modeling KDD Processes within the Inductive Database Framework
pp. 325
Cognitive Dimensions of Notations: Design Tools for Cognitive Technology
pp. 297
Scale Multi-commodity Flow Handling on Dynamic Networks
pp. 687
Bit-Sliding: A Generic Technique for Bit-Serial Implementations of SPN-based Primitives
pp. 358
The Definition of Transitive Closure with OCL – Limitations and Applications –
pp. 438
On Portability, Performance and Scalability of an MPI OpenCL Lattice Boltzmann Code
pp. 264
Agency and the Art of Interactive Digital Storytelling
pp. 302
Trust and Security Realization for Mobile Users in GSM Cellular Networks
pp. 510
A system for defeasible argumentation, with defeasible priorities
pp. 458
Simulation League: The Next Generation
pp. 464
A Comparison of a Brain-Computer Interface and an Eye Tracker: Is There a More Appropriate Technology for Controlling a Virtual Keyboard in an ALS Patient?
pp. 289
Workshop: Education in Interactive Digital Storytelling
pp. 343
Modeling Approach for Business Networks with an Integration and Business Perspective
pp. 771
Ocean: Object-Aware Anchor-Free Tracking
pp. 610
Performance evaluation of WASMII: a data driven computer on a virtual hardware
pp. 660
Combining Random Subspace Approach with smote Oversampling for Imbalanced Data Classification
pp. 756
A Case Study on Multi-Criteria Optimization of an Event Detection Software under Limited Budgets
pp. 737
A Physarum-Inspired Ant Colony Optimization for Community Mining
pp. 464
Efficient RDFS Entailment in External Memory
pp. 628
A New Direction in AI — Toward a Computational Theory of Perceptions
pp. 735
Using PNU-Based Techniques to Detect Alien Frames in Videos
pp. 652
FIRE in ImageCLEF 2005: Combining Content-Based Image Retrieval with Textual Information Retrieval
pp. 584
Mental Models of Menu Structures in Diabetes Assistants
pp. 824
Proposal of Ride Comfort Evaluation Method Using the EEG
pp. 869
Inferring Cognition from fMRI Brain Images
pp. 807
Zhang Neural Network Versus Gradient Neural Network for Online Time-Varying Quadratic Function Minimization
pp. 834
Online Sauter Diameter Measurement of Air Bubbles and Oil Drops in Stirred Bioreactors by Using Hough Transform
pp. 732
Mobile Computing in Medicine: Designing Mobile Questionnaires for Elderly and Partially Sighted People
pp. 1171
“BlindMath” a New Scientific Editor for Blind Students
Similar content
3,175
The Maple Case-Bearer Paraclemensia Acerifoliella Fitch
Authors:
Glenn Herrick
Proving the occurrence of Common Swift Apus apus pekinensis in the United Arab Emirates
Authors:
H. ROBERTS
,
O Campbell
CardioMEMS: Proving that Failure is not the only option for HF patients
Authors:
Carolyn Nissley
,
Justin D. Roberts
,
Lisa D. Rathman
…
See all similar
Cited by
4
A Brief Overview of PVS
Authors:
Sam Owre
,
Natarajan Shankar
Proof Assistant Decision Procedures for Formalizing Origami
Authors:
Cezary Kaliszyk
,
Tetsuo Ida
Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework
Authors:
Gabriel Dos Reis
,
David Matthews
,
Yue Li
See all cited by