A forward internal calculus for model generation in S4. (29th March 2021)
- Record Type:
- Journal Article
- Title:
- A forward internal calculus for model generation in S4. (29th March 2021)
- Main Title:
- A forward internal calculus for model generation in S4
- Authors:
- Fiorentini, Camillo
Ferrari, Mauro - Abstract:
- Abstract: We propose an internal calculus to check the satisfiability of a set of formulas in ${\boldsymbol {S4}}$ . Our calculus directly supports model extraction and is designed so to implement a forward proof-search strategy that can be understood as a top-down construction of a model. We prove that the extracted models have minimal height.
- Is Part Of:
- Journal of logic and computation. Volume 31:Number 3(2021)
- Journal:
- Journal of logic and computation
- Issue:
- Volume 31:Number 3(2021)
- Issue Display:
- Volume 31, Issue 3 (2021)
- Year:
- 2021
- Volume:
- 31
- Issue:
- 3
- Issue Sort Value:
- 2021-0031-0003-0000
- Page Start:
- 771
- Page End:
- 796
- Publication Date:
- 2021-03-29
- Subjects:
- Logic programming -- Periodicals
Logic, Symbolic and mathematical -- Periodicals
Computational complexity -- Periodicals
005.115 - Journal URLs:
- http://logcom.oxfordjournals.org/ ↗
http://ukcatalogue.oup.com/ ↗ - DOI:
- 10.1093/logcom/exab014 ↗
- Languages:
- English
- ISSNs:
- 0955-792X
- Deposit Type:
- Legaldeposit
- View Content:
- Available online (eLD content is only available in our Reading Rooms) ↗
- Physical Locations:
- British Library DSC - 5010.552200
British Library DSC - BLDSS-3PM
British Library HMNTS - ELD Digital store - Ingest File:
- 19753.xml