• 779 Citations
  • 16 h-Index
1987 …2019
If you made any changes in Pure these will be visible here soon.

Research Output 1987 2019

  • 779 Citations
  • 16 h-Index
  • 43 Article
  • 20 Conference contribution
  • 2 Chapter
  • 1 Conference article
Filter
Conference contribution
2016

Semantics for "enough-certainty" and fitting's embedding of classical logic in S4

Bana, G. & Okada, M., 2016 Aug 1, Computer Science Logic 2016, CSL 2016. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 62.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semantics
Security of data
Network protocols
2013
4 Citations (Scopus)

Computationally complete symbolic attacker and key exchange

Bana, G., Hasebe, K. & Okada, M., 2013, Proceedings of the ACM Conference on Computer and Communications Security. p. 1231-1246 16 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Cryptography
Network protocols
1 Citation (Scopus)

Husserl and hilbert on completeness and husserl's term rewrite-based theory of multiplicity

Okada, M., 2013, Leibniz International Proceedings in Informatics, LIPIcs. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 21. p. 4-19 16 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Tissue

Shape perception in chemistry

Hastings, J., Batchelor, C. & Okada, M., 2013, CEUR Workshop Proceedings. CEUR-WS, Vol. 1007. p. 83-94 12 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Molecules
Functional groups
Screening
2012
3 Citations (Scopus)

On the cognitive efficacy of euler diagrams in syllogistic reasoning: A relational perspective

Mineshima, K., Sato, Y., Takemura, R. & Okada, M., 2012, CEUR Workshop Proceedings. CEUR-WS, Vol. 854. p. 17-31 15 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Students
2010
7 Citations (Scopus)

Two types of diagrammatic inference systems: Natural deduction style and resolution style

Mineshima, K., Okada, M. & Takemura, R., 2010, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6170 LNAI. p. 99-114 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6170 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Natural Deduction
Diagram
Topological Relations
Correspondence
Style
2009
4 Citations (Scopus)

Computational semantics for first-order logical analysis of cryptographic protocols

Bana, G., Hasebe, K. & Okada, M., 2009, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5458 LNCS. p. 33-56 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5458 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Cryptographic Protocols
Semantics
Formal Model
First-order
Network protocols
6 Citations (Scopus)

Conservativity for a hierarchy of Euler and Venn reasoning systems

Mineshima, K., Okada, M. & Takemura, R., 2009, CEUR Workshop Proceedings. Vol. 510. p. 37-61 25 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semantics
2008
16 Citations (Scopus)

Diagrammatic reasoning system with euler circles: Theory and experiment design

Mineshima, K., Okada, M., Sato, Y. & Takemura, R., 2008, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5223 LNAI. p. 188-205 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5223 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Design of experiments
Euler
Circle
Reasoning
Experiment
2007
1 Citation (Scopus)

Remarks on semantic completeness for proof-terms with Laird's dual affine/intuitionistic λ-calculus

Okada, M. & Takemura, R., 2007, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4600 LNCS. p. 167-181 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4600 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Calculi
Semantics
Completeness
Calculus
Demonstrations
2006
2 Citations (Scopus)

Drug Interaction Ontology (DIO) and the resource-sensitive logical inferences

Okada, M., Sugimoto, Y., Yoshikawa, S. & Konagaya, A., 2006, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4060 LNCS. p. 616-642 27 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4060 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Drug interactions
Drug Interactions
Ontology
Drugs
Resources
1999
31 Citations (Scopus)

The calculus of algebraic constructions

Blanqui, F., Jouannaud, J. P. & Okada, M., 1999, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag, Vol. 1631. p. 301-316 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 1631).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Calculus
Abstract data types
Higher Order
Abstract Data Types
Generalise
1993

System description of LAMBDALG - A higher order algebraic specification language

Gui, Y. & Okada, M., 1993 Jan 1, Logic Programming and Automated Reasoning - 4th International Conference, LPAR 1993, Proceedings. Voronkov, A. (ed.). Springer Verlag, p. 354-356 3 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 698 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1991
80 Citations (Scopus)

A computation model for executable higher-order algebraic specification languages

Jouannaud, J. P. & Okada, M., 1991 Jul, Proceedings - Symposium on Logic in Computer Science. Publ by IEEE, p. 350-361 12 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Functional programming
Religious buildings
Specification languages
29 Citations (Scopus)

Satisfiability of systems of ordinal notations with the subterm property is decidable

Jouannaud, J. P. & Okada, M., 1991, Automata, Languages and Programming - 18th International Colloquium, Proceedings. Springer Verlag, Vol. 510 LNCS. p. 455-468 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 510 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Notation
1989
32 Citations (Scopus)

Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system

Okada, M., 1989 Jul 17, Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989. Association for Computing Machinery, Vol. Part F130182. p. 357-363 7 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Term Rewriting Systems
Typed lambda Calculus
Calculus
Arbitrary
Term
1988
3 Citations (Scopus)

A logical analysis on theory of conditional rewriting: Preliminary report

Okada, M., 1988 Jan 1, Conditional Term Rewriting Systems - 1st International Workshop, Proceedings. Kaplan, S. & Jouannaud, J-P. (eds.). Springer Verlag, p. 179-196 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 308 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Rewriting
43 Citations (Scopus)

Canonical conditional rewrite systems

Dershowitz, N., Okada, M. & Sivakumar, G., 1988 Jan 1, 9th International Conference on Automated Deduction, Proceedings. Springer Verlag, Vol. 310 LNCS. p. 538-549 12 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 310 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract data types
Specifications
Abstract Data Types
Restriction
Confluence
41 Citations (Scopus)

Confluence of conditional rewrite systems

Dershowitz, N., Okada, M. & Sivakumar, G., 1988 Jan 1, Conditional Term Rewriting Systems - 1st International Workshop, Proceedings. Springer Verlag, Vol. 308 LNCS. p. 31-44 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 308 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Functional programming
Religious buildings
Confluence
Logic programming
Specifications
32 Citations (Scopus)

Proof-theoretic techniques for term rewriting theory.

Dershowitz, N. & Okada, M., 1988, Proc Third Annu Symp on Logic in Comput Sci. Publ by IEEE, p. 104-111 8 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Religious buildings
Computer science