yusuke1997/dblp-id-title huggingface dataset:
An e-origami artwork of a big wing crane
Towards trajectory planning for a 6-degree-of-freedom robot manipulator considering the orientation of the end-effector using computer algebra
Origami folds in higher-dimension
5th International Symposium on Symbolic Computation in Software Science, SCSS 2013, Castle of Hagenberg, Austria
From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry
Automatic Staging via Partial Evaluation Techniques
Gröbner basis computation via learning
A stable computation of multivariarte apporximate GCD based on SVD and lifting technique
A rewrite-based computational model for functional logic programming
Asynchronous testing of real-time systems
Bit-size reduction of triangular sets in two and three variables
Faster bivariate lexicographic Groebner bases modulo x k
First-order theorem proving with power maps in semigroups
Generating Asymptotically Non-terminant Initial Variable Values for Linear Diagonalizable Programs
Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications
Implementing a stepper using delimited continuations
C2PDLS: A Combination of Combinatory and Converse PDL with Substitutions
Lebesgue Constants and Optimal Node Systems via Symbolic Computations
Usage of Invariants for Symbolic Verification of Requirements
Verification of a brick Wang tiling algorithm
7th International Symposium on Symbolic Computation in Software Science, SCSS 2016, Tokyo, Japan, March 28-31, 2016
Parametric Exploration of Rewriting Logic Computations
Private Profile Matching for Mobile Social Networks Based on Fuzzy Extractors
A Parallel Construction of the Symbolic Observation Graph: the Basis for Efficient Model Checking of Concurrent Systems
Solving estimation problems using minimax polynomials and Gröbner bases
Methods for solving the Post correspondence problem and certificate generation
Integration of a Decentralised Pattern Matching: Venue for a New Paradigm Intermarriage
Foundations of Haskell's Rewrite Rules Based on Higher-Kinded Polymorphic Rewrite Systems
Critical Pair Analysis in Nominal Rewriting
A Data Structure to Handle Large Sets of Equal Terms
6th International Symposium on Symbolic Computation in Software Science, SCSS 2014, Gammarth, La Marsa, Tunisia, December 7-8, 2014
Certification of Sorting Algorithms Using Theorema and Coq
Towards trajectory planning of a robot manipulator with computer algebra using Bézier curves for obstacle avoidance
Reasoning about the embedded shape of a qualitatively represented curve
Transforming Prefix-constrained or Controlled Rewrite Systems
A modified parallel F4 algorithm for shared and distributed memory architectures
Logical and Algebraic Views of a Knot Fold of a Regular Heptagon
Towards Verified Construction for Planar Class of a Qualitative Spatial Representation
νZ - Maximal Satisfaction with Z3
A Method to Prove Japanese Theorems and Others Appeared in Wasan Using Maxima
PDT Logic for Stream Reasoning in Multi-agent Systems
SCSS 2017, The 8th International Symposium on Symbolic Computation in Software Science 2017, April 6-9, 2017, Gammarth, Tunisia
Machine Learning of Coq Proof Guidance: First Experiments
Formal Development of Distributed Enumeration Algorithms By Refinement-Based Techniques
Software for indefinite integration
Riemann Surfaces, Branch Cuts and Charisma
The geometry of N-body orbits and the DFT (extended abstract)
Functional decomposition of sparse polynomials (short talk abstract)
Automatic Inference of Term Equivalence in Term Rewriting Systems
Automated Verification of Equivalence on Quantum Cryptographic Protocols
Mathematics of 21st Century: A Personal View
Some applications of Chinese Remainder Theorem codes with error-correction
A Mathematica module for Conformal Geometric Algebra and Origami Folding
Towards a Reliable Formal Framework for Enhancing Risk Assessment in Access Control Systems
Formal Analysis of Vehicular Crash Severity Using KeYmaera X
Formal Verification of ABCD Parameters Based Models for Transmission Lines
Symbolic Graph Query Solving
Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors
EON 2004, Evaluation of Ontology-based Tools, Proceedings of the 3rd International Workshop on Evaluation of Ontology-based Tools held at the 3rd International Semantic Web Conference ISWC 2004, 7th November 2004, Hiroshima Prince Hotel, Hiroshima, Japan
A Semantic Category Matching Approach to Ontology Alignment
A Formalization of Ontology Learning From Text
Collaborative Ontology Building with Wiki@nt - A Multi-agent Based Ontology Building Environment
Using Prompt Ontology-Comparison Tools in the EON Ontology Alignment Contest
Ontology Alignment with OLA
Sample Evaluation of Ontology-Matching Systems
SemTalk
Case Study: Using Protege to Convert the Travel Ontology to UML and OWL
Evaluating Ontology-Mapping Tools: Requirements and Experience
SemTalk EON2003 Semantic Web Export / Import Interface Test
Assessment of Ontology-based Tools: Systemizing the Scenario Approach
DOODLE-OWL: OWL-based Semi-Automatic Ontology Development Environment
Ontology Alignment - Karlsruhe
Domain natural language description for the experiment (Taken from OntoWeb deliverable 1.3)
Tracking Name Patterns in OWL Ontologies
Using XSLT for Interoperability: DOE and The Travelling Domain Experiment
Model-driven, Semantic Service Integration using COSMO Framework
EON2002, Proceedings of the OntoWeb-SIG3 Workshop at the 13th International Conference on Knowledge Engineering and Knowledge Management EKAW 2002, Siguenza (Spain), 30th September 2002
A Benchmark Suite for Evaluating the Performance of the WebODE Ontology Engineering Platform
Towards a benchmark for Semantic Web reasoners - an analysis of the DAML ontology library
The Integration of OntoClean in WebODE
Debugging OWL Ontologies - A Reality Check
Protégé
Benchmarking Reasoners for Multi-Ontology Applications
Synthesizing the Mediator with jABC/ABC
OntoTrack: Fast Browsing and Easy Editing of Large Ontologie
Terminae
WebODE
OilEd
DL-workbench: a metamodeling approach to ontology manipulation
Interoperability of Protege 2.0 beta and OilEd 3.5 in the Domain Knowledge of Osteoporosis
Integrating Ontology Storage and Ontology-based Applications Through Client-side Query and Transformations
OntoManager: A Workbench Environment to facilitate Ontology Management and Interoperability
Proceedings of the 5th International Workshop on Evaluation of Ontologies and Ontology-based Tools, EON2007, Co-located with the ISWC2007, Busan, Korea, November 11th, 2007
Semantic System Integration - Incorporating Rule based Semantic Bridges into BPEL Processes
Racer: A Core Inference Engine for the Semantic Web
Introduction to the Experiment
Evaluation experiment of ontology tools' interoperability with the WebODE ontology engineering workbench
TooCoM: a Tool to Operationalize an Ontology with the Conceptual Graph Model
Detecting Quality Problems in Semantic Metadata without the Presence of a Gold Standard
Using Protégé-2000 in Reuse Processes
OpenKnoME
Proceedings of the 6th International Workshop on Evaluation of Ontology-based Tools and the Semantic Web Service Challenge (EON-SWSC-2008), Tenerife, Spain, June 1-2, 2008
An Ontology-Driven Application to Improve the Prescription of Educational Resources to Parents of Premature Infants
Results of Taxonomic Evaluation of RDF(S) and DAML+OIL ontologies using RDF(S) and DAML+OIL Validation Tools and Ontology Platforms import services
Abductive Synthesis of the Mediator Scenario with jABC and GEM
Characterizing Knowledge on the Semantic Web with Watson
Data and Process Mediation Support for B2B Integration
Ontology Evolution within Ontology Editors
EON2003, Evaluation of Ontology-based Tools, Proceedings of the 2nd International Workshop on Evaluation of Ontology-based Tools held at the 2nd International Semantic Web Conference ISWC 2003, 20th October 2003 (Workshop day), Sundial Resort, Sanibel Island, Florida, USA
Evaluating Ontology Search
OntoEdit
Semantic Web Service Discovery and Selection: a Test Bed Scenario
Domain natural language description for the experiment
A Panoramic Approach to Integrated Evaluation of Ontologies in the Semantic Web
A domain ontology engineering tool with general ontologies and text corpus
Proof Pearl: The Termination Analysis of Terminator
Extending Higher-Order Unification to Support Proof Irrelevance
Predicate Subtyping with Predicate Sets
Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings
Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
Implementing a Real-Time Process Algebra in HOL
Formal Verification of Algorithm W: The Monomorphic Case
Constructing the real numbers in HOL
The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability)
Virtual Theories
Reasoning About Java Programs with Aliasing and Frame Conditions
Symbolic Functional Evaluation
Generating Designs Using an Algorithmic Register Transfer Language with Formal Semantics
Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings
Program Transformations and Refinements in HOL
A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem
Mizar's Soft Type System
Modelling Generic Hardware Structures by Abstract Datatypes
An Irrational Construction of R from Z
A Methodology for Reusable Hardware Proofs
Verified Optimizations for the Intel IA-64 Architecture
Recursive Families of Inductive Types
Human-Style Theorem Proving Using PVS
LCF Examples in HOL
Mechanizing a pi-Calculus Equivalence in HOL
Linking HOL to a VLSI CAD System
Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification
Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2
An Interface between Clam and HOL
Divider Circuit Verification with Model Checking and Theorem Proving
Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verification
Theorema
Mechanical Verification of Secure Distributed Systems in Higher Order Logic
A Certified Data Race Analysis for a Java-like Language
HOL-ML
A Full Formalisation of pi-Calculus Theory in the Calculus of Constructions
Studying the ML Module System in Hol
Formalizing the Trading Theorem for the Classification of Surfaces
Unification Based Induction
Introducing well-founded function definitions in HOL
Simplifying Deep Embedding: A Formalised Code Generator
Formalization of VHDL Synthesis Procedure in Higher-Order Logic
Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysis
Translating Specifications in VDM-SL to PVS
Formalizing the Logic-Automaton Connection
Implementing and Verifying Finite-State Machines Using Types in Higher-Order Logic
Formalization of Graph Search Algorithms and Its Applications
Proof Pearl: De Bruijn Terms Really Do Work
Hints in Unification
Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm)
Introduction to the HOL System
A Hoare Logic for the State Monad
Formal Hardware Verification in HOL and in Boyer-Moore: A Comparative Analysis
Using PVS to Prove Some Theorems Of David Parnas
Will This Be Formal?
Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circiut Behavior
Proof Normalization for a First-Order Formulation of Higher-Order Logic
Efficient Reasoning about Executable Specifications in Coq
Axiomatic Constructor Classes in Isabelle/HOLCF
A HOL Package for Reasoning about Relations Defined by Mutual Induction
Program Abstraction in a Higher-Order Logic Framework
Free-Style Theorem Proving
Formal Verification of IA-64 Division Algorithms
A Theory of Finite Maps
Representing Hierarchical Automata in Interactive Theorem Provers
Graph model of LAMBDA in Higher Order Logic
Domain Theory in HOL
HOL Light: An Overview
Using Decision Procedures with a Higher-Order Logic
Mechanized Operational Semantics via (Co)Induction
A Structured Set of Higher-Order Problems
Routing Information Protocol in HOL/SPIN
Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS
Importing Mathematics from HOL into Nuprl
Intel's Formal Verification Experience on the Willamette Development
Boyer-Moore Automation for the HOL System
Some Domain Theory and Denotational Semantics in Coq
Trace-Based Coinductive Operational Semantics for While
Formal Certification of a Resource-Aware Language Implementation
Implementing a Methodology for Formally Verifying RISC Processors in HOL
A HOL Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language
Reasoning with the Formal Definition of Standard ML in HOL
The Practical Verification of Microprocessor Designs
A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata
Informal
Verification of BDD Normalization
Programming and Computing in HOL
A Formal Approach to Probabilistic Termination
Sequent Schema for Derived Rules
Term Algebras with Length Function and Bounded Quantifier Alternation
Practical Tactics for Separation Logic
Java Program Verification via a JVM Deep Embedding in ACL2
Hierarchical Reflection
A Comparison of MDG and HOL for Hardware Verification
Weakest Precondition for General Recursive Programs Formalized in Coq
Formalization of Planar Graphs
Generating Embeddings from Denotational Descriptions
Formalizing a Modal Logic for CSS in the HOL Theorem Prover
A Decision Procedure for Geometry in Coq
Building Formal Method Tools in the Isabelle/Isar Framework
HOL Around the World
Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover
Let's Get Physical: Models and Methods for Real-World Security Protocols
Specifying Instruction-Set Architectures in HOL: A Primer
Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties
Extracting Purely Functional Contents from Logical Inductive Types
Alfa/Agda
An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstraction
Type Classes and Overloading in Higher-Order Logic
Deep Embedding VHDL
Design Choices in Specification Languages and Verification Systems
Symbolic Animation as a Proof Tool
Quotient Types: A Modular Approach
Transcendental Functions and Continuity Checking in PVS
PVS
Appendix: Conjectures Concerning Proof, Design, and Verification
A Note on Interactive Theorem Proving with Theorem Continuation Functions
Types, Maps and Separation Logic
Efficient Representation and Computation of Tableau Proofs
First-Order Automation for Higher-Order-Logic Theorem Proving
Mechanical Verification of Total Correctness through Diversion Verification Conditions
Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0
A Theory of Structured Model-Based Specifications in Isabelle/HOL
Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings
Certifying a Termination Criterion Based on Graphs, without Graphs
Implementational Issues for Verifying RISC-Pipeline Conflicts in HOL
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof
Proving Isomorphism of First-Order Logic Proof Systems in HOL
Using Coq to Verify Java Card Applet Isolation Properties
Mizar
A Lazy Approach to Fully-Expansive Theorem Proving
The Village Telephone System: A Case Study in Formal Software Engineering
MetaPRL - A Modular Logical Environment
Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals
Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL
Learning to use HOL
Providing Tractable Security Analysis in HOL
Graphical Theories of Interactive Systems: Can a Proof Assistant Help?
On the Utility of Formal Methods in the Development and Certification of Software
Mechanized Metatheory for the Masses: The PoplMark Challenge
Verification for Robust Specification
Isabelle/Isar
Complete Integer Decision Procedures as Derived Rules in HOL
Very Efficient Conversions
A Broader Class of Trees for Recursive Type Definitions for HOL
PuzzleTool : An Example of Programming Computation and Deduction
First Order Logic with Domain Conditions
A Graphical Tool for Proving Unity Progress
A Brief Overview of HOL4
The HOL-Omega Logic
Proving ML Type Soundness Within Coq
A Formalisation of the VHDL Simulation Cycle
Proof of Program Transformations
Nuprl
Explicit Universes for the Calculus of Constructions
Integrating Gandalf and HOL
Inductive Invariants for Nested Recursion
Stålmarck's Algorithm as a HOL Derived Rule
Abstraction Techniques for Modeling Real-World Interface Chips
Shallow Lazy Proofs
Imperative Functional Programming with Isabelle/HOL
Universal Algebra in Type Theory
Representing Higher-Order Logic Proofs in HOL
Combining Decision Procedures in the HOL System
An Interpretation of NODEN in HOL
Mechanical Proofs about a Non-repudiation Protocol
TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory
An Embedding of Timed Transition Systems in HOL
Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings
A Program Logic for Resource Verification
Dealing With Temporal Complexity in Hardware Verification
Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings
B Method
A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL
TAS - A Generic Window Inference System
A Tool for Data Refinement
A Higher-Order Calculus for Categories
A Verified Compiler for a Structured Assembly Language
Operational Semantics Based on Formal Symbolic Simulation
Aircraft Trajectory Modeling and Altering Algorithm Verification
Implementation and Use of Annotations in HOL
Click'n Prove: Interactive Proofs within Set Theory
Proof Presentation for Isabelle
Hardware Verification Using Co-induction in COQ
PM: A Proof Manager for HOL and Other Provers
A Formal Theory of Undirected Graphs in Higher-Order Logic
A Generic Network on Chip Model
A Formal Theory of Simulations Between Infinite Automata
A Design Structure for Higher Order Quotients
Representing WP Semantics in Isabelle/ZF
A Proof Tool for Reasoning About Functional Programs
Certifying the Fast Fourier Transform with Coq
Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings
Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering
Formalising Observer Theory for Environment-Sensitive Bisimulation
Using Isabelle to Prove Simple Theorems
Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings
Experiments with Finite Tree Automata in Coq
Proof Pearl: From Concrete to Functional Unparsing
Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings
On the use of the HOL system for Protocol Verification
Elements of Mathematical Analysis in PVS
Proof Based Computation
Deriving a Correct Computer
Report on the UCD Microcoded Viper Verification Project
Formal Specification and Verification of ARM6
Recording and Checking HOL Proofs
HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier
Verification of Composed Hardware Systems Using CCS
A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols
Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992
A Mechanical Proof of the Cook-Levin Theorem
Canonical Big Operators
Connecting Proof Checkers and Computer Algebra Using OpenMath
A Programming Logic for Java Bytecode Programs
On Formalization of Bicategory Theory
Weak Systems of Set Theory Related to HOL
A Package for Inductive Relation Definitions in HOL
HELM and the Semantic Math-Web
Industrial Application of Theorem Proving to System Level Design
Formalizing Basic First Order Model Theory
Deciding Cryptographic Protocol Adequacy with HOL: The Implementation
The Isabelle Framework
Program Extraction from Large Proof Developments
Why we can't have SML-style datatype Declarations in HOL
A Purely Definitional Universal Domain
A Proposal for a Formal OCL Semantics in Isabelle/HOL
Non-primitive Recursive Function Definitions
Formalizing Soundness of Contextual Effects
PhoX
Towards a HOL Theory and Memory
Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL
An Isabelle-Based Theorem Prover for VDM-SL
HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
Correct Embedded Computing Futures
Some Theorems We Should Prove
A Comparison of Two Proof Critics: Power vs. Robustness
Mizar Light for HOL Light
Developing an Interface for HOL
Formal Verification of Counterflow Pipeline Architecture
Five Axioms of Alpha-Conversion
A Parameterized Proof Manager
Deciding Cryptographic Protocol Adequacy with HOL
A Formalisation of Smallfoot in HOL
Abstract Theories in HOL
Free Variables and Subexpressions in Higher-Order Meta Logic
Psi-calculi in Isabelle
Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL
Proving Pearl: Knuth's Algorithm for Prime Numbers
Higher Order Rippling in IsaPlanner
A Report on ICL HOL
Towards an Object-Oriented Progification Language
Specification and Formal Synthesis of Digital Circuits
A HOL Theory of Euclidean Space
Verified LISP Implementations on ARM, x86 and PowerPC
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit
Proof Pearl: Revisiting the Mini-rubik in Coq
Towards a Machine-Checked Java Specification Book
Reasoning About CBV Functional Programs in Isabelle/HOL
Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions
The Need for Formal Verification in Hardware Design and What Formal Verification Has Not Done for Me Lately
Functional Procedures in Higher-Order Logic
Real Number Calculations and Theorem Proving
Case Studies in Compiler Correctness Using HOL
A Modular Formalisation of Finite Group Theory
Formal Verification of the Alpha 21364 Network Protocol
Formalizing the Proof of the Kepler Conjecture
Using XCAP to Certify Realistic Systems Code: Machine Context Management
The 5 Colour Theorem in Isabelle/Isar
Two-Level Meta-reasoning in Coq
Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain
A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion
Implementing Modules in the Coq System
Mechanizing Relevant Logics with HOL
HOLCF: Higher Order Logic of Computable Functions
View from the Fringe of the Fringe (Joint with CHARME 2001)
Formal Methods and Security Evaluation (Invited Talk)
A Better x86 Memory Model: x86-TSO
Verifying Second-Level Security Protocols
A Machine-Checked Theory of Floating Point Arithmetic
Theorem Reuse by Proof Term Transformation
Inductive Definitions: Automation and Application
Datatypes in L2
Case Studies in Meta-Level Theorem Proving
Window Inference in the HOL System
Verified Decision Procedures on Context-Free Grammars
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code
Separation Logic for Small-Step cminor
Primality Proving with Elliptic Curves
Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS
Improving the Result of High-Level Synthesis Using Interactive Transformational Design
An Informal Discussion of Issues in Mechanically-Assisted Reasoning
Highlighting the Lambda-free Fragment of Automath
Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings
Verifying the Accuracy of Polynomial Approximations in HOL
Mechanising the Temporal Logic of Actions in HOL
Formalizing Java Dynamic Loading in HOL
Deriving Correctness Properties of Compiled Code
Verified Bytecode Subroutines
A Simple Graph Theory and Its Application in Railway Signalling
Certified Exact Transcendental Real Number Computation in Coq