Partial correctness of an algorithm computing Lucas sequences
From MaRDI portal
Publication:6592315
DOI10.2478/forma-2020-0025zbMATH Open1543.68421MaRDI QIDQ6592315
Publication date: 26 August 2024
Published in: Formalized Mathematics (Search for Journal in Brave)
Number-theoretic algorithms; complexity (11Y16) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Fibonacci and Lucas numbers and polynomials and generalizations (11B39) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Four decades of {\textsc{Mizar}}. Foreword
- Proving properties of programs on hierarchical nominative data
- Implementation of the composition-nominative approach to program formalization in Mizar
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Simple-named complex-valued nominative data -- definition and basic operations
- Kleene algebra of partial predicates
- On algebras of algorithms and specifications over uninterpreted data
- On an algorithmic algebra over simple-named complex-valued nominative data
- An inference system of an extension of Floyd-Hoare logic for partial predicates
- Partial correctness of GCD algorithm
- Partial correctness of a factorial algorithm
- Partial correctness of a power algorithm
- Fibonacci and Lucas Numbers with Applications
- An axiomatic basis for computer programming
- General theory and tools for proving algorithms in nominative data systems
This page was built for publication: Partial correctness of an algorithm computing Lucas sequences
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6592315)
