Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 23
    • Merge requests 23
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #224
Closed
Open
Issue created Dec 18, 2018 by Ralf Jung@jungOwner

Define persistence otherwise (and get rid of core)

As a preparatory step towards defining the persistence modality inside the logic (if reasonably possible), we could try to change the model of persistence in Iris to no longer use the core (and get rid of the core). As long as persistence is the only connective defined using the core, it is impossible to define an equivalent connective inside the logic, so this is interesting both to simplify the RA axioms (and even more so the axioms for ordered RAs), and to work towards maybe eventually defining persistence inside the logic.

Cc @robbertkrebbers @jjourdan @jtassaro

Edited Aug 28, 2020 by Ralf Jung
Assignee
Assign to
Time tracking